{ (Cl (BDD (L~ (Cage C,i)))) where i is Element of NAT : verum } c= bool the carrier of (TOP-REAL 2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Cl (BDD (L~ (Cage C,i)))) where i is Element of NAT : verum } or x in bool the carrier of (TOP-REAL 2) )
assume x in { (Cl (BDD (L~ (Cage C,i)))) where i is Element of NAT : verum } ; :: thesis: x in bool the carrier of (TOP-REAL 2)
then ex i being Element of NAT st x = Cl (BDD (L~ (Cage C,i))) ;
hence x in bool the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence BDD-Family C is Subset-Family of (TOP-REAL 2) ; :: thesis: verum