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

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