theorem Th25: :: FILTER_0:25

for L being Lattice
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 )