TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8
.= TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) by PCOMPS_1:def 5 ;
then reconsider W = C as Subset of (Euclid n) ;
take diameter W ; :: thesis: ex W being Subset of (Euclid n) st
( W = C & diameter W = diameter W )
take W ; :: thesis: ( W = C & diameter W = diameter W )
thus ( W = C & diameter W = diameter W ) ; :: thesis: verum