set X = {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))};
{A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} c= bool the carrier of T

proof

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

end;

hence {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} is Subset-Family of T ; :: thesis: verum