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 iff p <=> q in F ) by Def13;
hence ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) by Def12; :: thesis: verum