theorem Th74: :: FILTER_2:74

for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 ) by Th73;