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