XX: TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) = TopSpaceMetr (Euclid 0) by EUCLID:def 8;
then the carrier of (TOP-REAL 0) is 1 -element ;
then TOP-REAL 0 is 1 -element by STRUCT_0:def 19;
hence Family_open_set (Euclid 0) = {{},{{}}} by XX, JORDAN2C:105, YELLOW_9:9; :: thesis: verum