let S be Subset of L; :: thesis: ( S is empty implies ( S is initial & S is final ) )
assume Z: S is empty ; :: thesis: ( S is initial & S is final )
thus S is initial :: thesis: S is final

proof

let p be Element of L; :: according to LATTICES:def 22 :: thesis: for q being Element of L st p [= q & q in S holds
p in S
thus for q being Element of L st p [= q & q in S holds
p in S by Z; :: thesis: verum

end;

let p be Element of L; :: according to LATTICES:def 23 :: thesis: for q being Element of L st p [= q & p in S holds
q in S
thus for q being Element of L st p [= q & p in S holds
q in S by Z; :: thesis: verum