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 lower & S is upper )
thus S is lower ; :: thesis: S is upper
let x be Element of L; :: according to WAYBEL_0:def 20 :: thesis: for y being Element of L st x in S & x <= y holds
y in S
thus for y being Element of L st x in S & x <= y holds
y in S ; :: thesis: verum