set X1 = {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )};
set X2 = {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )};
{A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} c= bool the carrier of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} or x in bool the carrier of T )
assume x in {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} ; :: thesis: x in bool the carrier of T
then ( x = A or x = Cl A or x = (Cl A) ` or x = Cl ((Cl A) ` ) or x = (Cl ((Cl A) ` )) ` or x = Cl ((Cl ((Cl A) ` )) ` ) or x = (Cl ((Cl ((Cl A) ` )) ` )) ` ) by ENUMSET1:def 5;
hence x in bool the carrier of T ; :: thesis: verum

end;

then reconsider X1 = {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} as Subset-Family of T ;
{(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} c= bool the carrier of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} or x in bool the carrier of T )
assume x in {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} ; :: thesis: x in bool the carrier of T
then ( x = A ` or x = Cl (A ` ) or x = (Cl (A ` )) ` or x = Cl ((Cl (A ` )) ` ) or x = (Cl ((Cl (A ` )) ` )) ` or x = Cl ((Cl ((Cl (A ` )) ` )) ` ) or x = (Cl ((Cl ((Cl (A ` )) ` )) ` )) ` ) by ENUMSET1:def 5;
hence x in bool the carrier of T ; :: thesis: verum

end;

then reconsider X2 = {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} as Subset-Family of T ;
X1 \/ X2 is Subset-Family of T ;
hence {A,(A - ),((A - ) ` ),(((A - ) ` ) - ),((((A - ) ` ) - ) ` ),(((((A - ) ` ) - ) ` ) - ),((((((A - ) ` ) - ) ` ) - ) ` )} \/ {(A ` ),((A ` ) - ),(((A ` ) - ) ` ),((((A ` ) - ) ` ) - ),(((((A ` ) - ) ` ) - ) ` ),((((((A ` ) - ) ` ) - ) ` ) - ),(((((((A ` ) - ) ` ) - ) ` ) - ) ` )} is Subset-Family of T ; :: thesis: verum