let x1, x2, x3, x4, x5, x6, x7, x8, x9 be object ; :: thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}

now :: thesis: for x being object 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 object ; :: 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:2; :: thesis: verum