:: deftheorem Def8 defines TOP-REAL EUCLID:def 8 :
for n being Nat
for b₂ being strict RLTopStruct holds
( b₂ = TOP-REAL n iff ( TopStruct(# the carrier of b₂, the topology of b₂ #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b₂, the ZeroF of b₂, the addF of b₂, the Mult of b₂ #) = RealVectSpace (Seg n) ) );