let L be Lattice; :: thesis: for p, q being Element of L
for F being Filter of L
for p', q' being Element of (latt F) st p = p' & q = q' holds
( p [= q iff p' [= q' )
let p, q be Element of L; :: thesis: for F being Filter of L
for p', q' being Element of (latt F) st p = p' & q = q' holds
( p [= q iff p' [= q' )
let F be Filter of L; :: thesis: for p', q' being Element of (latt F) st p = p' & q = q' holds
( p [= q iff p' [= q' )
let p', q' be Element of (latt F); :: thesis: ( p = p' & q = q' implies ( p [= q iff p' [= q' ) )
assume ( p = p' & q = q' ) ; :: thesis: ( p [= q iff p' [= q' )
then ( ( p [= q implies p "\/" q = q ) & ( p "\/" q = q implies p [= q ) & ( p' [= q' implies p' "\/" q' = q' ) & ( p' "\/" q' = q' implies p' [= q' ) & p' "\/" q' = p "\/" q & q = q' ) by Th64, LATTICES:def 3;
hence ( p [= q iff p' [= q' ) ; :: thesis: verum