theorem Th51: :: FILTER_0:51

for L being Lattice
for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 ) by Th50;