let T be RelStr ; :: thesis: RelStr(# the carrier of T,the InternalRel of T #) is SubSpace of T
set S = RelStr(# the carrier of T,the InternalRel of T #);
for x being Element of RelStr(# the carrier of T,the InternalRel of T #) st x in the carrier of RelStr(# the carrier of T,the InternalRel of T #) holds
U_FT x = (Im the InternalRel of T,x) /\ the carrier of T by XBOOLE_1:28;
hence RelStr(# the carrier of T,the InternalRel of T #) is SubSpace of T by Def2; :: thesis: verum