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 object ; :: 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 ;
{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 object ; :: 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 ;
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