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

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