theorem Th77: :: FILTER_2:77

for L being Lattice
for P being non empty ClosedSubset of L st L is distributive holds
latt (L,P) is distributive