the carrier of L c= the carrier of L ;
then reconsider S = the carrier of L as Subset of L ;
take S ; :: thesis: ( S is infs-closed & S is sups-closed & not S is empty )
thus subrelstr S is infs-inheriting :: according to WAYBEL23:def 3 :: thesis: ( S is sups-closed & not S is empty )

proof

the carrier of (subrelstr S) = S by YELLOW_0:def 15;
then for X being Subset of (subrelstr S) st ex_inf_of X,L holds
"/\" X,L in the carrier of (subrelstr S) ;
hence subrelstr S is infs-inheriting by YELLOW_0:def 18; :: thesis: verum

end;

thus subrelstr S is sups-inheriting :: according to WAYBEL23:def 4 :: thesis: not S is empty

proof

the carrier of (subrelstr S) = S by YELLOW_0:def 15;
then for X being Subset of (subrelstr S) st ex_sup_of X,L holds
"\/" X,L in the carrier of (subrelstr S) ;
hence subrelstr S is sups-inheriting by YELLOW_0:def 19; :: thesis: verum

end;

thus not S is empty ; :: thesis: verum