let L be Lattice; :: thesis: for p, q being Element of L
for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
let p, q be Element of L; :: thesis: for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
let F be Filter of L; :: thesis: ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
( ( p,q are_equivalence_wrt F implies p <=> q in F ) & ( p <=> q in F implies p,q are_equivalence_wrt F ) & ( [p,q] in equivalence_wrt F implies p <=> q in F ) & ( p <=> q in F implies [p,q] in equivalence_wrt F ) ) by Def12, Def13;
hence ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) ; :: thesis: verum