let a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 be object ; :: thesis: {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} = {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10}
thus {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} c= {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} :: according to XBOOLE_0:def 10 :: thesis: {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} c= {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} or x in {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} )
assume x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} ; :: thesis: x in {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10}
then ( x in {a1} or x in {a2,a3,a4,a5,a6,a7,a8,a9,a10} ) by XBOOLE_0:def 3;
then ( x = a1 or x = a2 or x = a3 or x = a4 or x = a5 or x = a6 or x = a7 or x = a8 or x = a9 or x = a10 ) by TARSKI:def 1, ENUMSET1:def 7;
hence x in {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} by ENUMSET1:def 8; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} or x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} )
assume x in {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} ; :: thesis: x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10}
then ( x = a1 or x = a2 or x = a3 or x = a4 or x = a5 or x = a6 or x = a7 or x = a8 or x = a9 or x = a10 ) by ENUMSET1:def 8;
then ( x in {a1} or x in {a2,a3,a4,a5,a6,a7,a8,a9,a10} ) by TARSKI:def 1, ENUMSET1:def 7;
hence x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9,a10} by XBOOLE_0:def 3; :: thesis: verum