deffunc H1( set ) -> Element of K32( the carrier of T) = (Im ( the InternalRel of T,$1)) /\ P;
A1:
for x being Element of T st x in P holds
H1(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) = H1(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 b1 being non empty strict SubSpace of T st [#] b1 = P
; verum