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 EUCLID:77, YELLOW_9:9; :: thesis: verum