theorem Th72: :: FILTER_2:72

for L being Lattice
for P being non empty ClosedSubset of L holds
( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )