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