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