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 that
A1: L is 0_Lattice and
A2: Bottom L in D ; :: thesis: ( <.D.) = <.L.) & <.D.) = the carrier of L )
A3: <.(Bottom L).) = <.L.) by A1, Th17;
hence ( <.D.) c= <.L.) & <.L.) c= <.D.) ) by A2, Th23; :: 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 A2, A3, Th23; :: according to XBOOLE_0:def 10 :: thesis: verum