set S = RelStr(# the carrier of L,the InternalRel of L #);
RelStr(# the carrier of L,the InternalRel of L #) is SubRelStr of L

proof

thus the carrier of RelStr(# the carrier of L,the InternalRel of L #) c= the carrier of L ; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of RelStr(# the carrier of L,the InternalRel of L #) c= the InternalRel of L
thus the InternalRel of RelStr(# the carrier of L,the InternalRel of L #) c= the InternalRel of L ; :: thesis: verum

end;

then reconsider S = RelStr(# the carrier of L,the InternalRel of L #) as SubRelStr of L ;
take S ; :: thesis: ( not S is empty & S is full & S is strict )
thus not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: ( S is full & S is strict )
thus the InternalRel of S = the InternalRel of L |_2 the carrier of S by XBOOLE_1:28; :: according to YELLOW_0:def 14 :: thesis: S is strict
thus S is strict ; :: thesis: verum