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