[ BeginEnv "axiom"
, BracketL
, Word "extensionality"
, BracketR
, Label "ext"
, Word "suppose"
, Word "for"
, Word "all"
, BeginEnv "math"
, Variable "a"
, EndEnv "math"
, Word "we"
, Word "have"
, BeginEnv "math"
, Variable "a"
, Command "in"
, Variable "A"
, EndEnv "math"
, Word "iff"
, BeginEnv "math"
, Variable "a"
, Command "in"
, Variable "B"
, EndEnv "math"
, Symbol "."
, Word "then"
, BeginEnv "math"
, Variable "A"
, Symbol "="
, Variable "B"
, EndEnv "math"
, Symbol "."
, EndEnv "axiom"
, BeginEnv "axiom"
, Label "union_defn"
, Word "let"
, BeginEnv "math"
, Variable "A"
, Symbol ","
, Variable "B"
, EndEnv "math"
, Word "be"
, Word "sets"
, Symbol "."
, BeginEnv "math"
, Variable "a"
, Command "in"
, Variable "A"
, Command "union"
, Variable "B"
, EndEnv "math"
, Word "iff"
, BeginEnv "math"
, Variable "a"
, Command "in"
, Variable "A"
, EndEnv "math"
, Word "or"
, BeginEnv "math"
, Variable "a"
, Command "in"
, Variable "B"
, EndEnv "math"
, Symbol "."
, EndEnv "axiom"
, BeginEnv "proposition"
, Label "union_comm"
, BeginEnv "math"
, Variable "A"
, Command "union"
, Variable "B"
, Symbol "="
, Variable "B"
, Command "union"
, Variable "A"
, EndEnv "math"
, Symbol "."
, EndEnv "proposition"
, BeginEnv "proposition"
, Label "union_assoc"
, BeginEnv "math"
, ParenL
, Variable "A"
, Command "union"
, Variable "B"
, ParenR
, Command "union"
, Variable "C"
, Symbol "="
, Variable "A"
, Command "union"
, ParenL
, Variable "B"
, Command "union"
, Variable "C"
, ParenR
, EndEnv "math"
, Symbol "."
, EndEnv "proposition"
, BeginEnv "proof"
, Word "for"
, Word "all"
, BeginEnv "math"
, Variable "a"
, EndEnv "math"
, Word "we"
, Word "have"
, Word "if"
, BeginEnv "math"
, Variable "a"
, Command "in"
, ParenL
, Variable "A"
, Command "union"
, Variable "B"
, ParenR
, Command "union"
, Variable "C"
, EndEnv "math"
, Symbol ","
, Word "then"
, BeginEnv "math"
, Variable "a"
, Command "in"
, Variable "A"
, Command "union"
, ParenL
, Variable "B"
, Command "union"
, Variable "C"
, ParenR
, EndEnv "math"
, Symbol "."
, Word "for"
, Word "all"
, BeginEnv "math"
, Variable "a"
, EndEnv "math"
, Word "we"
, Word "have"
, Word "if"
, BeginEnv "math"
, Variable "a"
, Command "in"
, Variable "A"
, Command "union"
, ParenL
, Variable "B"
, Command "union"
, Variable "C"
, ParenR
, EndEnv "math"
, Symbol ","
, Word "then"
, BeginEnv "math"
, Variable "a"
, Command "in"
, ParenL
, Variable "A"
, Command "union"
, Variable "B"
, ParenR
, Command "union"
, Variable "C"
, EndEnv "math"
, Symbol "."
, EndEnv "proof"
]