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