( the carrier of L c= the carrier of L & the InternalRel of L |_2 the carrier of L = the InternalRel of L ) by XBOOLE_1:28;
then reconsider S = RelStr(# the carrier of L, the InternalRel of L #) as non empty strict full SubRelStr of L by Th57;
take S ; :: thesis: ( S is infs-inheriting & S is sups-inheriting & not S is empty & S is full & S is strict )
thus S is infs-inheriting :: thesis: ( S is sups-inheriting & not S is empty & S is full & S is strict )

proof

let X be Subset of S; :: according to YELLOW_0:def 18 :: thesis: ( ex_inf_of X,L implies "/\" (X,L) in the carrier of S )
thus ( ex_inf_of X,L implies "/\" (X,L) in the carrier of S ) ; :: thesis: verum

end;

thus S is sups-inheriting :: thesis: ( not S is empty & S is full & S is strict )

proof

let X be Subset of S; :: according to YELLOW_0:def 19 :: thesis: ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S )
thus ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) ; :: thesis: verum

end;

thus ( not S is empty & S is full & S is strict ) ; :: thesis: verum