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

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