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₁ being RelStr st
( 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₁ ) ) ; :: thesis: verum