deffunc H_{1}( 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

H_{1}(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_{1}(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_{1} being non empty strict SubSpace of T st [#] b_{1} = P
; :: thesis: verum

A1: for x being Element of T st x in P holds

H

consider G being Relation of P such that

A2: for y being Element of T st y in P holds

Im (G,y) = H

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