let L be Lattice; :: thesis: ( L is 0_Lattice implies <.L.) = <.(Bottom L).) )
assume L is 0_Lattice ; :: thesis: <.L.) = <.(Bottom L).)
then reconsider L9 = L as 0_Lattice ;
thus <.L.) c= <.(Bottom L).) :: according to XBOOLE_0:def 10 :: thesis: <.(Bottom L).) c= <.L.)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <.L.) or x in <.(Bottom L).) )
assume x in <.L.) ; :: thesis: x in <.(Bottom L).)
then reconsider x = x as Element of L9 ;
( Bottom L in <.(Bottom L).) & x "/\" (Bottom L9) = Bottom L9 ) ;
hence x in <.(Bottom L).) by Th8; :: thesis: verum

end;

thus <.(Bottom L).) c= <.L.) ; :: thesis: verum