:: deftheorem Def2 defines SubSpace FINTOPO6:def 2 :
for T, b₂ being RelStr holds
( b₂ is SubSpace of T iff ( the carrier of b₂ c= the carrier of T & ( for x being Element of b₂ st x in the carrier of b₂ holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b₂ ) ) );