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

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

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