thus [#] L is initial :: thesis: ( [#] L is final & not [#] L is empty )

proof

let p, q be Element of L; :: according to LATTICES:def 22 :: thesis: ( p [= q & q in [#] L implies p in [#] L )
thus ( p [= q & q in [#] L implies p in [#] L ) ; :: thesis: verum

end;

thus [#] L is final :: thesis: not [#] L is empty

proof

let p, q be Element of L; :: according to LATTICES:def 23 :: thesis: ( p [= q & p in [#] L implies q in [#] L )
thus ( p [= q & p in [#] L implies q in [#] L ) ; :: thesis: verum

end;

thus not [#] L is empty ; :: thesis: verum