{ (UBD (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 { (UBD (L~ (Cage (C,i)))) where i is Nat : verum } or x in bool the carrier of (TOP-REAL 2) )
assume x in { (UBD (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 = UBD (L~ (Cage (C,i))) ;
hence x in bool the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

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