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 )
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 ; :: according to WAYBEL23:def 3 :: thesis: ( S is sups-closed & not S is empty )
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 ; :: according to WAYBEL23:def 4 :: thesis: not S is empty
thus not S is empty ; :: thesis: verum