deffunc H₁( set ) -> Element of K18(the carrier of T) = (Im the InternalRel of T,$1) /\ P;
A1: for x being Element of T st x in P holds
H₁(x) c= P by XBOOLE_1:17;
consider G being Relation of P such that
A2: for y being Element of T st y in P holds
Im G,y = H₁(y) from RELSET_1:sch 3(A1);
set FS = RelStr(# P,G #);
for x being Element of RelStr(# P,G #) st x in the carrier of RelStr(# P,G #) holds
U_FT x = (Im the InternalRel of T,x) /\ the carrier of RelStr(# P,G #) by A2;
then ( [#] RelStr(# P,G #) = the carrier of RelStr(# P,G #) & RelStr(# P,G #) is non empty strict SubSpace of T ) by Def2;
hence ex b₁ being non empty strict SubSpace of T st [#] b₁ = P ; :: thesis: verum