theorem Th17: :: FILTER_0:17

for L being Lattice st L is 0_Lattice holds
<.L.) = <.(Bottom L).)