set S = RelStr(# the carrier of L, the InternalRel of L #);
reconsider S = RelStr(# the carrier of L, the InternalRel of L #) as SubRelStr of L by Def13;
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