TopStruct(# the carrier of (TOP-REAL 0 ),the topology of (TOP-REAL 0 ) #) = TopSpaceMetr (Euclid 0 ) by EUCLID:def 8;
hence Family_open_set (Euclid 0 ) = {{} ,{{} }} by YELLOW_9:9, JORDAN2C:113; :: thesis: verum