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

now :: thesis: for x being object holds
( x in {x1,x2,x3,x4,x5,x6} iff x in {x1,x2,x3} \/ {x4,x5,x6} )

let x be object ; :: 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:2; :: thesis: verum