let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be object ; :: thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} c= {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10} :: according to XBOOLE_0:def 10 :: thesis: {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10} c= {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} or x in {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10} )
assume x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} ; :: thesis: x in {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10}
then ( 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 ENUMSET1:def 8;
then ( x in {x1,x2,x3,x4,x5} or x in {x6,x7,x8,x9,x10} ) by ENUMSET1:def 3;
hence x in {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10} by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10} or x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} )
assume x in {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9,x10} ; :: thesis: x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10}

per cases then ( x in {x1,x2,x3,x4,x5} or x in {x6,x7,x8,x9,x10} ) by XBOOLE_0:def 3;

suppose x in {x1,x2,x3,x4,x5} ; :: thesis: x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10}

then ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) by ENUMSET1:def 3;
hence x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} by ENUMSET1:def 8; :: thesis: verum

end;

suppose x in {x6,x7,x8,x9,x10} ; :: thesis: x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10}

then ( x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) by ENUMSET1:def 3;
hence x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} by ENUMSET1:def 8; :: thesis: verum

end;

end;