for x being Element of T st x in the carrier of T holds

U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of T by XBOOLE_1:28;

hence ex b_{1} being RelStr st

( the carrier of b_{1} c= the carrier of T & ( for x being Element of b_{1} st x in the carrier of b_{1} holds

U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b_{1} ) )
; :: thesis: verum

U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of T by XBOOLE_1:28;

hence ex b

( the carrier of b

U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b