:: ENUMSET1 semantic presentation begin Lm1: for x, X, y being set holds ( x in union {X,{y}} iff ( x in X or x = y ) ) proof let x, X, y be set ; ::_thesis: ( x in union {X,{y}} iff ( x in X or x = y ) ) A1: ( not x in union {X,{y}} or x in X or x in {y} ) proof assume x in union {X,{y}} ; ::_thesis: ( x in X or x in {y} ) then ex Z being set st ( x in Z & Z in {X,{y}} ) by TARSKI:def_4; hence ( x in X or x in {y} ) by TARSKI:def_2; ::_thesis: verum end; A2: ( x in {y} iff x = y ) by TARSKI:def_1; ( X in {X,{y}} & {y} in {X,{y}} ) by TARSKI:def_2; hence ( x in union {X,{y}} iff ( x in X or x = y ) ) by A1, A2, TARSKI:def_4; ::_thesis: verum end; definition let x1, x2, x3 be set ; func{x1,x2,x3} -> set means :Def1: :: ENUMSET1:def 1 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) proof take union {{x1,x2},{x3}} ; ::_thesis: for x being set holds ( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) ) ( x in {x1,x2} iff ( x = x1 or x = x2 ) ) by TARSKI:def_2; hence ( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def1 defines { ENUMSET1:def_1_:_ for x1, x2, x3, b4 being set holds ( b4 = {x1,x2,x3} iff for x being set holds ( x in b4 iff ( x = x1 or x = x2 or x = x3 ) ) ); definition let x1, x2, x3, x4 be set ; func{x1,x2,x3,x4} -> set means :Def2: :: ENUMSET1:def 2 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) proof take union {{x1,x2,x3},{x4}} ; ::_thesis: for x being set holds ( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ( x in {x1,x2,x3} iff ( x = x1 or x = x2 or x = x3 ) ) by Def1; hence ( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 or \$1 = x4 ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def2 defines { ENUMSET1:def_2_:_ for x1, x2, x3, x4, b5 being set holds ( b5 = {x1,x2,x3,x4} iff for x being set holds ( x in b5 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ); definition let x1, x2, x3, x4, x5 be set ; func{x1,x2,x3,x4,x5} -> set means :Def3: :: ENUMSET1:def 3 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) proof take union {{x1,x2,x3,x4},{x5}} ; ::_thesis: for x being set holds ( x in union {{x1,x2,x3,x4},{x5}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4},{x5}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2; hence ( x in union {{x1,x2,x3,x4},{x5}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 or \$1 = x4 or \$1 = x5 ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def3 defines { ENUMSET1:def_3_:_ for x1, x2, x3, x4, x5, b6 being set holds ( b6 = {x1,x2,x3,x4,x5} iff for x being set holds ( x in b6 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ); definition let x1, x2, x3, x4, x5, x6 be set ; func{x1,x2,x3,x4,x5,x6} -> set means :Def4: :: ENUMSET1:def 4 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) proof take union {{x1,x2,x3,x4,x5},{x6}} ; ::_thesis: for x being set holds ( x in union {{x1,x2,x3,x4,x5},{x6}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5},{x6}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ( x in {x1,x2,x3,x4,x5} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) by Def3; hence ( x in union {{x1,x2,x3,x4,x5},{x6}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 or \$1 = x4 or \$1 = x5 or \$1 = x6 ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def4 defines { ENUMSET1:def_4_:_ for x1, x2, x3, x4, x5, x6, b7 being set holds ( b7 = {x1,x2,x3,x4,x5,x6} iff for x being set holds ( x in b7 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ); definition let x1, x2, x3, x4, x5, x6, x7 be set ; func{x1,x2,x3,x4,x5,x6,x7} -> set means :Def5: :: ENUMSET1:def 5 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) proof take union {{x1,x2,x3,x4,x5,x6},{x7}} ; ::_thesis: for x being set holds ( x in union {{x1,x2,x3,x4,x5,x6},{x7}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6},{x7}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ( x in {x1,x2,x3,x4,x5,x6} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) by Def4; hence ( x in union {{x1,x2,x3,x4,x5,x6},{x7}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 or \$1 = x4 or \$1 = x5 or \$1 = x6 or \$1 = x7 ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def5 defines { ENUMSET1:def_5_:_ for x1, x2, x3, x4, x5, x6, x7, b8 being set holds ( b8 = {x1,x2,x3,x4,x5,x6,x7} iff for x being set holds ( x in b8 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ); definition let x1, x2, x3, x4, x5, x6, x7, x8 be set ; func{x1,x2,x3,x4,x5,x6,x7,x8} -> set means :Def6: :: ENUMSET1:def 6 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) proof take union {{x1,x2,x3,x4,x5,x6,x7},{x8}} ; ::_thesis: for x being set holds ( x in union {{x1,x2,x3,x4,x5,x6,x7},{x8}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6,x7},{x8}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ( x in {x1,x2,x3,x4,x5,x6,x7} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) by Def5; hence ( x in union {{x1,x2,x3,x4,x5,x6,x7},{x8}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 or \$1 = x4 or \$1 = x5 or \$1 = x6 or \$1 = x7 or \$1 = x8 ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def6 defines { ENUMSET1:def_6_:_ for x1, x2, x3, x4, x5, x6, x7, x8, b9 being set holds ( b9 = {x1,x2,x3,x4,x5,x6,x7,x8} iff for x being set holds ( x in b9 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ); definition let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; func{x1,x2,x3,x4,x5,x6,x7,x8,x9} -> set means :Def7: :: ENUMSET1:def 7 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) proof take union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} ; ::_thesis: for x being set holds ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ( x in {x1,x2,x3,x4,x5,x6,x7,x8} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) by Def6; hence ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 or \$1 = x4 or \$1 = x5 or \$1 = x6 or \$1 = x7 or \$1 = x8 or \$1 = x9 ); thus for X, Y being set st ( for x being set holds ( x in X iff S1[x] ) ) & ( for x being set holds ( x in Y iff S1[x] ) ) holds X = Y from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def7 defines { ENUMSET1:def_7_:_ for x1, x2, x3, x4, x5, x6, x7, x8, x9, b10 being set holds ( b10 = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being set holds ( x in b10 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ); definition let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be set ; func{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> set means :Def8: :: ENUMSET1:def 8 for x being set holds ( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) proof take union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} ; ::_thesis: for x being set holds ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) by Def7; hence ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) by Lm1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ) & ( for x being set holds ( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 = x1 or \$1 = x2 or \$1 = x3 or \$1 = x4 or \$1 = x5 or \$1 = x6 or \$1 = x7 or \$1 = x8 or \$1 = x9 or \$1 = x10 ); thus for X, Y being set st ( for x being set holds ( x in X iff S1[x] ) ) & ( for x being set holds ( x in Y iff S1[x] ) ) holds X = Y from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def8 defines { ENUMSET1:def_8_:_ for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, b11 being set holds ( b11 = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for x being set holds ( x in b11 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ); theorem Th1: :: ENUMSET1:1 for x1, x2 being set holds {x1,x2} = {x1} \/ {x2} proof let x1, x2 be set ; ::_thesis: {x1,x2} = {x1} \/ {x2} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2}_iff_x_in_{x1}_\/_{x2}_) let x be set ; ::_thesis: ( x in {x1,x2} iff x in {x1} \/ {x2} ) ( x in {x1,x2} iff ( x = x1 or x = x2 ) ) by TARSKI:def_2; then ( x in {x1,x2} iff ( x in {x1} or x in {x2} ) ) by TARSKI:def_1; hence ( x in {x1,x2} iff x in {x1} \/ {x2} ) by XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2} = {x1} \/ {x2} by TARSKI:1; ::_thesis: verum end; theorem Th2: :: ENUMSET1:2 for x1, x2, x3 being set holds {x1,x2,x3} = {x1} \/ {x2,x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x1} \/ {x2,x3} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3}_iff_x_in_{x1}_\/_{x2,x3}_) let x be set ; ::_thesis: ( x in {x1,x2,x3} iff x in {x1} \/ {x2,x3} ) ( x in {x1,x2,x3} iff ( x = x1 or x = x2 or x = x3 ) ) by Def1; then ( x in {x1,x2,x3} iff ( x in {x1} or x in {x2,x3} ) ) by TARSKI:def_1, TARSKI:def_2; hence ( x in {x1,x2,x3} iff x in {x1} \/ {x2,x3} ) by XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3} = {x1} \/ {x2,x3} by TARSKI:1; ::_thesis: verum end; theorem Th3: :: ENUMSET1:3 for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x2} \/ {x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x1,x2} \/ {x3} thus {x1,x2,x3} = {x1} \/ {x2,x3} by Th2 .= {x1} \/ ({x2} \/ {x3}) by Th1 .= ({x1} \/ {x2}) \/ {x3} by XBOOLE_1:4 .= {x1,x2} \/ {x3} by Th1 ; ::_thesis: verum end; Lm2: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3,x4}_iff_x_in_{x1,x2}_\/_{x3,x4}_) let x be set ; ::_thesis: ( x in {x1,x2,x3,x4} iff x in {x1,x2} \/ {x3,x4} ) ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2; then ( x in {x1,x2,x3,x4} iff ( x in {x1,x2} or x in {x3,x4} ) ) by TARSKI:def_2; hence ( x in {x1,x2,x3,x4} iff x in {x1,x2} \/ {x3,x4} ) by XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by TARSKI:1; ::_thesis: verum end; theorem Th4: :: ENUMSET1:4 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} thus {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2 .= ({x1} \/ {x2}) \/ {x3,x4} by Th1 .= {x1} \/ ({x2} \/ {x3,x4}) by XBOOLE_1:4 .= {x1} \/ {x2,x3,x4} by Th2 ; ::_thesis: verum end; theorem :: ENUMSET1:5 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2; theorem Th6: :: ENUMSET1:6 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} thus {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2 .= {x1,x2} \/ ({x3} \/ {x4}) by Th1 .= ({x1,x2} \/ {x3}) \/ {x4} by XBOOLE_1:4 .= {x1,x2,x3} \/ {x4} by Th3 ; ::_thesis: verum end; Lm3: for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} proof let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3,x4,x5}_iff_x_in_{x1,x2,x3}_\/_{x4,x5}_) let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5} iff x in {x1,x2,x3} \/ {x4,x5} ) ( x in {x1,x2,x3,x4,x5} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) by Def3; then ( x in {x1,x2,x3,x4,x5} iff ( x in {x1,x2,x3} or x in {x4,x5} ) ) by Def1, TARSKI:def_2; hence ( x in {x1,x2,x3,x4,x5} iff x in {x1,x2,x3} \/ {x4,x5} ) by XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by TARSKI:1; ::_thesis: verum end; theorem Th7: :: ENUMSET1:7 for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} proof let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} thus {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3 .= ({x1} \/ {x2,x3}) \/ {x4,x5} by Th2 .= {x1} \/ ({x2,x3} \/ {x4,x5}) by XBOOLE_1:4 .= {x1} \/ {x2,x3,x4,x5} by Lm2 ; ::_thesis: verum end; theorem Th8: :: ENUMSET1:8 for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5} proof let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5} thus {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3 .= ({x1,x2} \/ {x3}) \/ {x4,x5} by Th3 .= {x1,x2} \/ ({x3} \/ {x4,x5}) by XBOOLE_1:4 .= {x1,x2} \/ {x3,x4,x5} by Th2 ; ::_thesis: verum end; theorem :: ENUMSET1:9 for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3; theorem Th10: :: ENUMSET1:10 for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5} proof let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5} thus {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3 .= {x1,x2,x3} \/ ({x4} \/ {x5}) by Th1 .= ({x1,x2,x3} \/ {x4}) \/ {x5} by XBOOLE_1:4 .= {x1,x2,x3,x4} \/ {x5} by Th6 ; ::_thesis: verum end; Lm4: for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3,x4,x5,x6}_iff_x_in_{x1,x2,x3}_\/_{x4,x5,x6}_) let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6} iff x in {x1,x2,x3} \/ {x4,x5,x6} ) ( x in {x1,x2,x3,x4,x5,x6} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) by Def4; then ( x in {x1,x2,x3,x4,x5,x6} iff ( x in {x1,x2,x3} or x in {x4,x5,x6} ) ) by Def1; hence ( x in {x1,x2,x3,x4,x5,x6} iff x in {x1,x2,x3} \/ {x4,x5,x6} ) by XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by TARSKI:1; ::_thesis: verum end; theorem Th11: :: ENUMSET1:11 for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4 .= ({x1} \/ {x2,x3}) \/ {x4,x5,x6} by Th2 .= {x1} \/ ({x2,x3} \/ {x4,x5,x6}) by XBOOLE_1:4 .= {x1} \/ {x2,x3,x4,x5,x6} by Th8 ; ::_thesis: verum end; theorem Th12: :: ENUMSET1:12 for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6} thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4 .= ({x1,x2} \/ {x3}) \/ {x4,x5,x6} by Th3 .= {x1,x2} \/ ({x3} \/ {x4,x5,x6}) by XBOOLE_1:4 .= {x1,x2} \/ {x3,x4,x5,x6} by Th4 ; ::_thesis: verum end; theorem :: ENUMSET1:13 for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4; theorem Th14: :: ENUMSET1:14 for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6} thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4 .= {x1,x2,x3} \/ ({x4} \/ {x5,x6}) by Th2 .= ({x1,x2,x3} \/ {x4}) \/ {x5,x6} by XBOOLE_1:4 .= {x1,x2,x3,x4} \/ {x5,x6} by Th6 ; ::_thesis: verum end; theorem :: ENUMSET1:15 for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6} thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4 .= {x1,x2,x3} \/ ({x4,x5} \/ {x6}) by Th3 .= ({x1,x2,x3} \/ {x4,x5}) \/ {x6} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5} \/ {x6} by Lm3 ; ::_thesis: verum end; Lm5: for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3,x4,x5,x6,x7}_iff_x_in_{x1,x2,x3,x4}_\/_{x5,x6,x7}_) let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7} ) A1: ( x in {x5,x6,x7} iff ( x = x5 or x = x6 or x = x7 ) ) by Def1; ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2; hence ( x in {x1,x2,x3,x4,x5,x6,x7} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7} ) by A1, Def5, XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by TARSKI:1; ::_thesis: verum end; theorem Th16: :: ENUMSET1:16 for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5 .= ({x1} \/ {x2,x3,x4}) \/ {x5,x6,x7} by Th4 .= {x1} \/ ({x2,x3,x4} \/ {x5,x6,x7}) by XBOOLE_1:4 .= {x1} \/ {x2,x3,x4,x5,x6,x7} by Lm4 ; ::_thesis: verum end; theorem Th17: :: ENUMSET1:17 for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2} \/ {x3,x4,x5,x6,x7} proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2} \/ {x3,x4,x5,x6,x7} thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5 .= ({x1,x2} \/ {x3,x4}) \/ {x5,x6,x7} by Lm2 .= {x1,x2} \/ ({x3,x4} \/ {x5,x6,x7}) by XBOOLE_1:4 .= {x1,x2} \/ {x3,x4,x5,x6,x7} by Th8 ; ::_thesis: verum end; theorem Th18: :: ENUMSET1:18 for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3} \/ {x4,x5,x6,x7} proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3} \/ {x4,x5,x6,x7} thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5 .= ({x1,x2,x3} \/ {x4}) \/ {x5,x6,x7} by Th6 .= {x1,x2,x3} \/ ({x4} \/ {x5,x6,x7}) by XBOOLE_1:4 .= {x1,x2,x3} \/ {x4,x5,x6,x7} by Th4 ; ::_thesis: verum end; theorem :: ENUMSET1:19 for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5; theorem :: ENUMSET1:20 for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5} \/ {x6,x7} proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5} \/ {x6,x7} thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5 .= {x1,x2,x3,x4} \/ ({x5} \/ {x6,x7}) by Th2 .= ({x1,x2,x3,x4} \/ {x5}) \/ {x6,x7} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5} \/ {x6,x7} by Th10 ; ::_thesis: verum end; theorem :: ENUMSET1:21 for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7} proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7} thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5 .= {x1,x2,x3,x4} \/ ({x5,x6} \/ {x7}) by Th3 .= ({x1,x2,x3,x4} \/ {x5,x6}) \/ {x7} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5,x6} \/ {x7} by Th14 ; ::_thesis: verum end; Lm6: for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} proof let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3,x4,x5,x6,x7,x8}_iff_x_in_{x1,x2,x3,x4}_\/_{x5,x6,x7,x8}_) let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7,x8} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8} ) A1: ( x in {x5,x6,x7,x8} iff ( x = x5 or x = x6 or x = x7 or x = x8 ) ) by Def2; ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2; hence ( x in {x1,x2,x3,x4,x5,x6,x7,x8} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8} ) by A1, Def6, XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by TARSKI:1; ::_thesis: verum end; theorem :: ENUMSET1:22 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} proof let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6 .= ({x1} \/ {x2,x3,x4}) \/ {x5,x6,x7,x8} by Th4 .= {x1} \/ ({x2,x3,x4} \/ {x5,x6,x7,x8}) by XBOOLE_1:4 .= {x1} \/ {x2,x3,x4,x5,x6,x7,x8} by Th18 ; ::_thesis: verum end; theorem Th23: :: ENUMSET1:23 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8} proof let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8} thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6 .= ({x1,x2} \/ {x3,x4}) \/ {x5,x6,x7,x8} by Lm2 .= {x1,x2} \/ ({x3,x4} \/ {x5,x6,x7,x8}) by XBOOLE_1:4 .= {x1,x2} \/ {x3,x4,x5,x6,x7,x8} by Th12 ; ::_thesis: verum end; theorem Th24: :: ENUMSET1:24 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8} proof let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8} thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6 .= ({x1,x2,x3} \/ {x4}) \/ {x5,x6,x7,x8} by Th6 .= {x1,x2,x3} \/ ({x4} \/ {x5,x6,x7,x8}) by XBOOLE_1:4 .= {x1,x2,x3} \/ {x4,x5,x6,x7,x8} by Th7 ; ::_thesis: verum end; theorem :: ENUMSET1:25 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6; theorem :: ENUMSET1:26 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8} proof let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8} thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6 .= {x1,x2,x3,x4} \/ ({x5} \/ {x6,x7,x8}) by Th4 .= ({x1,x2,x3,x4} \/ {x5}) \/ {x6,x7,x8} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5} \/ {x6,x7,x8} by Th10 ; ::_thesis: verum end; theorem :: ENUMSET1:27 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8} proof let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8} thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6 .= {x1,x2,x3,x4} \/ ({x5,x6} \/ {x7,x8}) by Lm2 .= ({x1,x2,x3,x4} \/ {x5,x6}) \/ {x7,x8} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5,x6} \/ {x7,x8} by Th14 ; ::_thesis: verum end; theorem :: ENUMSET1:28 for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8} proof let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8} thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6 .= {x1,x2,x3,x4} \/ ({x5,x6,x7} \/ {x8}) by Th6 .= ({x1,x2,x3,x4} \/ {x5,x6,x7}) \/ {x8} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5,x6,x7} \/ {x8} by Lm5 ; ::_thesis: verum end; theorem Th29: :: ENUMSET1:29 for x1 being set holds {x1,x1} = {x1} proof let x1 be set ; ::_thesis: {x1,x1} = {x1} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x1}_iff_x_in_{x1}_) let x be set ; ::_thesis: ( x in {x1,x1} iff x in {x1} ) ( x in {x1,x1} iff x = x1 ) by TARSKI:def_2; hence ( x in {x1,x1} iff x in {x1} ) by TARSKI:def_1; ::_thesis: verum end; hence {x1,x1} = {x1} by TARSKI:1; ::_thesis: verum end; theorem Th30: :: ENUMSET1:30 for x1, x2 being set holds {x1,x1,x2} = {x1,x2} proof let x1, x2 be set ; ::_thesis: {x1,x1,x2} = {x1,x2} thus {x1,x1,x2} = {x1,x1} \/ {x2} by Th3 .= {x1} \/ {x2} by Th29 .= {x1,x2} by Th1 ; ::_thesis: verum end; theorem Th31: :: ENUMSET1:31 for x1, x2, x3 being set holds {x1,x1,x2,x3} = {x1,x2,x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x1,x2,x3} = {x1,x2,x3} thus {x1,x1,x2,x3} = {x1,x1} \/ {x2,x3} by Lm2 .= {x1} \/ {x2,x3} by Th29 .= {x1,x2,x3} by Th2 ; ::_thesis: verum end; theorem Th32: :: ENUMSET1:32 for x1, x2, x3, x4 being set holds {x1,x1,x2,x3,x4} = {x1,x2,x3,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x2,x3,x4} = {x1,x2,x3,x4} thus {x1,x1,x2,x3,x4} = {x1,x1} \/ {x2,x3,x4} by Th8 .= {x1} \/ {x2,x3,x4} by Th29 .= {x1,x2,x3,x4} by Th4 ; ::_thesis: verum end; theorem Th33: :: ENUMSET1:33 for x1, x2, x3, x4, x5 being set holds {x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5} proof let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5} thus {x1,x1,x2,x3,x4,x5} = {x1,x1} \/ {x2,x3,x4,x5} by Th12 .= {x1} \/ {x2,x3,x4,x5} by Th29 .= {x1,x2,x3,x4,x5} by Th7 ; ::_thesis: verum end; theorem Th34: :: ENUMSET1:34 for x1, x2, x3, x4, x5, x6 being set holds {x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6} thus {x1,x1,x2,x3,x4,x5,x6} = {x1,x1} \/ {x2,x3,x4,x5,x6} by Th17 .= {x1} \/ {x2,x3,x4,x5,x6} by Th29 .= {x1,x2,x3,x4,x5,x6} by Th11 ; ::_thesis: verum end; theorem Th35: :: ENUMSET1:35 for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7} proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7} thus {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x1} \/ {x2,x3,x4,x5,x6,x7} by Th23 .= {x1} \/ {x2,x3,x4,x5,x6,x7} by Th29 .= {x1,x2,x3,x4,x5,x6,x7} by Th16 ; ::_thesis: verum end; theorem :: ENUMSET1:36 for x1 being set holds {x1,x1,x1} = {x1} proof let x1 be set ; ::_thesis: {x1,x1,x1} = {x1} thus {x1,x1,x1} = {x1,x1} by Th30 .= {x1} by Th29 ; ::_thesis: verum end; theorem Th37: :: ENUMSET1:37 for x1, x2 being set holds {x1,x1,x1,x2} = {x1,x2} proof let x1, x2 be set ; ::_thesis: {x1,x1,x1,x2} = {x1,x2} thus {x1,x1,x1,x2} = {x1,x1,x2} by Th31 .= {x1,x2} by Th30 ; ::_thesis: verum end; theorem Th38: :: ENUMSET1:38 for x1, x2, x3 being set holds {x1,x1,x1,x2,x3} = {x1,x2,x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x2,x3} = {x1,x2,x3} thus {x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th32 .= {x1,x2,x3} by Th31 ; ::_thesis: verum end; theorem Th39: :: ENUMSET1:39 for x1, x2, x3, x4 being set holds {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4} thus {x1,x1,x1,x2,x3,x4} = {x1,x1,x2,x3,x4} by Th33 .= {x1,x2,x3,x4} by Th32 ; ::_thesis: verum end; theorem Th40: :: ENUMSET1:40 for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5} proof let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5} thus {x1,x1,x1,x2,x3,x4,x5} = {x1,x1,x2,x3,x4,x5} by Th34 .= {x1,x2,x3,x4,x5} by Th33 ; ::_thesis: verum end; theorem Th41: :: ENUMSET1:41 for x1, x2, x3, x4, x5, x6 being set holds {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6} thus {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x1,x2,x3,x4,x5,x6} by Th35 .= {x1,x2,x3,x4,x5,x6} by Th34 ; ::_thesis: verum end; theorem :: ENUMSET1:42 for x1 being set holds {x1,x1,x1,x1} = {x1} proof let x1 be set ; ::_thesis: {x1,x1,x1,x1} = {x1} thus {x1,x1,x1,x1} = {x1,x1} by Th37 .= {x1} by Th29 ; ::_thesis: verum end; theorem Th43: :: ENUMSET1:43 for x1, x2 being set holds {x1,x1,x1,x1,x2} = {x1,x2} proof let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x2} = {x1,x2} thus {x1,x1,x1,x1,x2} = {x1,x1,x2} by Th38 .= {x1,x2} by Th30 ; ::_thesis: verum end; theorem Th44: :: ENUMSET1:44 for x1, x2, x3 being set holds {x1,x1,x1,x1,x2,x3} = {x1,x2,x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x1,x2,x3} = {x1,x2,x3} thus {x1,x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th39 .= {x1,x2,x3} by Th31 ; ::_thesis: verum end; theorem Th45: :: ENUMSET1:45 for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4} thus {x1,x1,x1,x1,x2,x3,x4} = {x1,x1,x2,x3,x4} by Th40 .= {x1,x2,x3,x4} by Th32 ; ::_thesis: verum end; theorem Th46: :: ENUMSET1:46 for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5} proof let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5} thus {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x1,x2,x3,x4,x5} by Th41 .= {x1,x2,x3,x4,x5} by Th33 ; ::_thesis: verum end; theorem :: ENUMSET1:47 for x1 being set holds {x1,x1,x1,x1,x1} = {x1} proof let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1} = {x1} thus {x1,x1,x1,x1,x1} = {x1,x1} by Th43 .= {x1} by Th29 ; ::_thesis: verum end; theorem Th48: :: ENUMSET1:48 for x1, x2 being set holds {x1,x1,x1,x1,x1,x2} = {x1,x2} proof let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x1,x2} = {x1,x2} thus {x1,x1,x1,x1,x1,x2} = {x1,x1,x2} by Th44 .= {x1,x2} by Th30 ; ::_thesis: verum end; theorem Th49: :: ENUMSET1:49 for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3} thus {x1,x1,x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th45 .= {x1,x2,x3} by Th31 ; ::_thesis: verum end; theorem Th50: :: ENUMSET1:50 for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4} thus {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x1,x2,x3,x4} by Th46 .= {x1,x2,x3,x4} by Th32 ; ::_thesis: verum end; theorem :: ENUMSET1:51 for x1 being set holds {x1,x1,x1,x1,x1,x1} = {x1} proof let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1} = {x1} thus {x1,x1,x1,x1,x1,x1} = {x1,x1} by Th48 .= {x1} by Th29 ; ::_thesis: verum end; theorem Th52: :: ENUMSET1:52 for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x2} = {x1,x2} proof let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x2} = {x1,x2} thus {x1,x1,x1,x1,x1,x1,x2} = {x1,x1,x2} by Th49 .= {x1,x2} by Th30 ; ::_thesis: verum end; theorem Th53: :: ENUMSET1:53 for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3} thus {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th50 .= {x1,x2,x3} by Th31 ; ::_thesis: verum end; theorem :: ENUMSET1:54 for x1 being set holds {x1,x1,x1,x1,x1,x1,x1} = {x1} proof let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x1} = {x1} thus {x1,x1,x1,x1,x1,x1,x1} = {x1,x1} by Th52 .= {x1} by Th29 ; ::_thesis: verum end; theorem Th55: :: ENUMSET1:55 for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2} proof let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2} thus {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x1,x2} by Th53 .= {x1,x2} by Th30 ; ::_thesis: verum end; theorem :: ENUMSET1:56 for x1 being set holds {x1,x1,x1,x1,x1,x1,x1,x1} = {x1} proof let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x1,x1} = {x1} thus {x1,x1,x1,x1,x1,x1,x1,x1} = {x1,x1} by Th55 .= {x1} by Th29 ; ::_thesis: verum end; theorem Th57: :: ENUMSET1:57 for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x3,x2} proof let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x1,x3,x2} thus {x1,x2,x3} = {x1} \/ {x2,x3} by Th2 .= {x1,x3,x2} by Th2 ; ::_thesis: verum end; theorem Th58: :: ENUMSET1:58 for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x1,x3} proof let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x2,x1,x3} thus {x1,x2,x3} = {x1,x2} \/ {x3} by Th3 .= {x2,x1,x3} by Th3 ; ::_thesis: verum end; theorem Th59: :: ENUMSET1:59 for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x3,x1} proof let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x2,x3,x1} thus {x1,x2,x3} = {x2,x3} \/ {x1} by Th2 .= {x2,x3,x1} by Th3 ; ::_thesis: verum end; theorem Th60: :: ENUMSET1:60 for x1, x2, x3 being set holds {x1,x2,x3} = {x3,x2,x1} proof let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x3,x2,x1} thus {x1,x2,x3} = {x3,x1,x2} by Th59 .= {x3,x2,x1} by Th57 ; ::_thesis: verum end; theorem Th61: :: ENUMSET1:61 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x4,x3} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x2,x4,x3} thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4 .= {x1} \/ {x2,x4,x3} by Th57 .= {x1,x2,x4,x3} by Th4 ; ::_thesis: verum end; theorem :: ENUMSET1:62 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x2,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x3,x2,x4} thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4 .= {x1} \/ {x3,x2,x4} by Th58 .= {x1,x3,x2,x4} by Th4 ; ::_thesis: verum end; theorem Th63: :: ENUMSET1:63 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x4,x2} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x3,x4,x2} thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4 .= {x1} \/ {x3,x4,x2} by Th59 .= {x1,x3,x4,x2} by Th4 ; ::_thesis: verum end; theorem Th64: :: ENUMSET1:64 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x4,x3,x2} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x4,x3,x2} thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4 .= {x1} \/ {x4,x3,x2} by Th60 .= {x1,x4,x3,x2} by Th4 ; ::_thesis: verum end; theorem Th65: :: ENUMSET1:65 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x3,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x1,x3,x4} thus {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by Th6 .= {x2,x1,x3} \/ {x4} by Th58 .= {x2,x1,x3,x4} by Th6 ; ::_thesis: verum end; Lm7: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x3,x1,x4} thus {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by Th6 .= {x2,x3,x1} \/ {x4} by Th59 .= {x2,x3,x1,x4} by Th6 ; ::_thesis: verum end; theorem :: ENUMSET1:66 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x4,x3} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x1,x4,x3} thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7 .= {x2,x1,x4,x3} by Th63 ; ::_thesis: verum end; theorem :: ENUMSET1:67 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7; theorem :: ENUMSET1:68 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x4,x1} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x3,x4,x1} thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7 .= {x2,x3,x4,x1} by Th61 ; ::_thesis: verum end; theorem Th69: :: ENUMSET1:69 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x1,x3} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x4,x1,x3} thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7 .= {x2,x4,x1,x3} by Th64 ; ::_thesis: verum end; theorem :: ENUMSET1:70 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x3,x1} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x4,x3,x1} thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7 .= {x2,x4,x3,x1} by Th63 ; ::_thesis: verum end; Lm8: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x2,x1,x4} thus {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by Th6 .= {x3,x2,x1} \/ {x4} by Th60 .= {x3,x2,x1,x4} by Th6 ; ::_thesis: verum end; theorem :: ENUMSET1:71 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8; theorem :: ENUMSET1:72 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x4,x1} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x2,x4,x1} thus {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8 .= {x3,x2,x4,x1} by Th61 ; ::_thesis: verum end; theorem :: ENUMSET1:73 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x1,x2} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x4,x1,x2} thus {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8 .= {x3,x4,x1,x2} by Th64 ; ::_thesis: verum end; theorem Th74: :: ENUMSET1:74 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x2,x1} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x4,x2,x1} thus {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8 .= {x3,x4,x2,x1} by Th63 ; ::_thesis: verum end; theorem :: ENUMSET1:75 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x2,x3,x1} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x4,x2,x3,x1} thus {x1,x2,x3,x4} = {x3,x4,x2,x1} by Th74 .= {x4,x2,x3,x1} by Lm7 ; ::_thesis: verum end; theorem :: ENUMSET1:76 for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x3,x2,x1} proof let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x4,x3,x2,x1} thus {x1,x2,x3,x4} = {x3,x4,x2,x1} by Th74 .= {x4,x3,x2,x1} by Th65 ; ::_thesis: verum end; Lm9: for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3,x4,x5,x6,x7,x8,x9}_iff_x_in_{x1,x2,x3,x4}_\/_{x5,x6,x7,x8,x9}_) let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} ) A1: ( x in {x5,x6,x7,x8,x9} iff ( x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) by Def3; ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2; hence ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} ) by A1, Def7, XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by TARSKI:1; ::_thesis: verum end; theorem :: ENUMSET1:77 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9} thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9 .= ({x1} \/ {x2,x3,x4}) \/ {x5,x6,x7,x8,x9} by Th4 .= {x1} \/ ({x2,x3,x4} \/ {x5,x6,x7,x8,x9}) by XBOOLE_1:4 .= {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9} by Th24 ; ::_thesis: verum end; theorem :: ENUMSET1:78 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9} thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9 .= ({x1,x2} \/ {x3,x4}) \/ {x5,x6,x7,x8,x9} by Lm2 .= {x1,x2} \/ ({x3,x4} \/ {x5,x6,x7,x8,x9}) by XBOOLE_1:4 .= {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9} by Th17 ; ::_thesis: verum end; theorem :: ENUMSET1:79 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9} thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9 .= ({x1,x2,x3} \/ {x4}) \/ {x5,x6,x7,x8,x9} by Th6 .= {x1,x2,x3} \/ ({x4} \/ {x5,x6,x7,x8,x9}) by XBOOLE_1:4 .= {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9} by Th11 ; ::_thesis: verum end; theorem :: ENUMSET1:80 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9; theorem :: ENUMSET1:81 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9} thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9 .= {x1,x2,x3,x4} \/ ({x5} \/ {x6,x7,x8,x9}) by Th7 .= ({x1,x2,x3,x4} \/ {x5}) \/ {x6,x7,x8,x9} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9} by Th10 ; ::_thesis: verum end; theorem :: ENUMSET1:82 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9} thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9 .= {x1,x2,x3,x4} \/ ({x5,x6} \/ {x7,x8,x9}) by Th8 .= ({x1,x2,x3,x4} \/ {x5,x6}) \/ {x7,x8,x9} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9} by Th14 ; ::_thesis: verum end; theorem :: ENUMSET1:83 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9} thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9 .= {x1,x2,x3,x4} \/ ({x5,x6,x7} \/ {x8,x9}) by Lm3 .= ({x1,x2,x3,x4} \/ {x5,x6,x7}) \/ {x8,x9} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9} by Lm5 ; ::_thesis: verum end; theorem :: ENUMSET1:84 for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9} thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9 .= {x1,x2,x3,x4} \/ ({x5,x6,x7,x8} \/ {x9}) by Th10 .= ({x1,x2,x3,x4} \/ {x5,x6,x7,x8}) \/ {x9} by XBOOLE_1:4 .= {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9} by Lm6 ; ::_thesis: verum end; theorem :: ENUMSET1:85 for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} proof let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} now__::_thesis:_for_x_being_set_holds_ (_x_in_{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10}_iff_x_in_{x1,x2,x3,x4,x5,x6,x7,x8,x9}_\/_{x10}_) let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} ) A1: ( x in {x10} iff x = x10 ) by TARSKI:def_1; ( ( ( not x = x1 & not x = x2 & not x = x3 & not x = x4 & not x = x5 & not x = x6 & not x = x7 & not x = x8 & not x = x9 & not x = x10 ) or x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} or x = x10 ) & ( ( not x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} & not x = x10 ) or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) by Def7; hence ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} ) by A1, Def8, XBOOLE_0:def_3; ::_thesis: verum end; hence {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} by TARSKI:1; ::_thesis: verum end; begin theorem :: ENUMSET1:86 for x, y, z being set st x <> y & x <> z holds {x,y,z} \ {x} = {y,z} proof let x, y, z be set ; ::_thesis: ( x <> y & x <> z implies {x,y,z} \ {x} = {y,z} ) assume A1: ( x <> y & x <> z ) ; ::_thesis: {x,y,z} \ {x} = {y,z} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {y,z} c= {x,y,z} \ {x} let a be set ; ::_thesis: ( a in {x,y,z} \ {x} implies a in {y,z} ) assume A2: a in {x,y,z} \ {x} ; ::_thesis: a in {y,z} then a in {x,y,z} by XBOOLE_0:def_5; then A3: ( a = x or a = y or a = z ) by Def1; not a in {x} by A2, XBOOLE_0:def_5; hence a in {y,z} by A3, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {y,z} or a in {x,y,z} \ {x} ) assume a in {y,z} ; ::_thesis: a in {x,y,z} \ {x} then A4: ( a = y or a = z ) by TARSKI:def_2; then A5: not a in {x} by A1, TARSKI:def_1; a in {x,y,z} by A4, Def1; hence a in {x,y,z} \ {x} by A5, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: ENUMSET1:87 for x1, x2, x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3} proof let x1, x2, x3 be set ; ::_thesis: {x2,x1} \/ {x3,x1} = {x1,x2,x3} thus {x2,x1} \/ {x3,x1} = {x2,x1,x3,x1} by Lm2 .= {x1,x1,x2,x3} by Th69 .= {x1,x2,x3} by Th31 ; ::_thesis: verum end;