let L be Lattice; :: thesis: for D being non empty Subset of L st L is 0_Lattice & Bottom L in D holds
( <.D.) = <.L.) & <.D.) = the carrier of L )
let D be non empty Subset of L; :: thesis: ( L is 0_Lattice & Bottom L in D implies ( <.D.) = <.L.) & <.D.) = the carrier of L ) )
assume ( L is 0_Lattice & Bottom L in D ) ; :: thesis: ( <.D.) = <.L.) & <.D.) = the carrier of L )
then A1: ( <.(Bottom L).) = <.L.) & <.(Bottom L).) c= <.D.) & <.L.) = the carrier of L ) by Th20, Th29;
hence ( <.D.) c= <.L.) & <.L.) c= <.D.) ) ; :: according to XBOOLE_0:def 10 :: thesis: <.D.) = the carrier of L
thus ( <.D.) c= the carrier of L & the carrier of L c= <.D.) ) by A1; :: according to XBOOLE_0:def 10 :: thesis: verum