let L be Lattice; :: thesis: 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 )
let p, q be Element of L; :: thesis: 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 )
let F be Filter of L; :: thesis: for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p9, q9 be Element of (latt F); :: thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 [= q9 ) )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def 3;
A2: ( p9 [= q9 iff p9 "\/" q9 = q9 ) by LATTICES:def 3;
assume ( p = p9 & q = q9 ) ; :: thesis: ( p [= q iff p9 [= q9 )
hence ( p [= q iff p9 [= q9 ) by A1, A2, Th64; :: thesis: verum