let a1, a2, a3, a4, a5, a6, a7, a8, a9 be object ; :: thesis: {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} = {a1,a2,a3,a4,a5,a6,a7,a8,a9}
thus {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} c= {a1,a2,a3,a4,a5,a6,a7,a8,a9} :: according to XBOOLE_0:def 10 :: thesis: {a1,a2,a3,a4,a5,a6,a7,a8,a9} c= {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} or x in {a1,a2,a3,a4,a5,a6,a7,a8,a9} )
assume x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} ; :: thesis: x in {a1,a2,a3,a4,a5,a6,a7,a8,a9}
then ( x in {a1} or x in {a2,a3,a4,a5,a6,a7,a8,a9} ) 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 ) by TARSKI:def 1, ENUMSET1:def 6;
hence x in {a1,a2,a3,a4,a5,a6,a7,a8,a9} by ENUMSET1:def 7; :: 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} or x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} )
assume x in {a1,a2,a3,a4,a5,a6,a7,a8,a9} ; :: thesis: x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9}
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 ) by ENUMSET1:def 7;
then ( x in {a1} or x in {a2,a3,a4,a5,a6,a7,a8,a9} ) by TARSKI:def 1, ENUMSET1:def 6;
hence x in {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9} by XBOOLE_0:def 3; :: thesis: verum