{ (Cl (BDD (L~ (Cage (C,i))))) where i is Nat : verum } c= bool the carrier of (TOP-REAL 2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Cl (BDD (L~ (Cage (C,i))))) where i is Nat : verum } or x in bool the carrier of (TOP-REAL 2) )
assume x in { (Cl (BDD (L~ (Cage (C,i))))) where i is Nat : verum } ; :: thesis: x in bool the carrier of (TOP-REAL 2)
then ex i being 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