let a1, a2, a3, a4, a5, a6, a7, a8, a9 be object ; {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}
XBOOLE_0:def 10 {a1,a2,a3,a4,a5,a6,a7,a8,a9} c= {a1} \/ {a2,a3,a4,a5,a6,a7,a8,a9}proof
let x be
object ;
TARSKI:def 3 ( 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}
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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}
; 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; verum