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: ( S is strict & S is full )
thus S is strict ; :: thesis: S is full
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: verum