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