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