theorem Th70: :: FILTER_2:70

for L being Lattice
for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .: