let L be Lattice; :: thesis: for p, q being Element of L
for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
let p, q be Element of L; :: thesis: for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
let F be Filter of L; :: thesis: ( p,q are_equivalence_wrt F implies q,p are_equivalence_wrt F )
assume p <=> q in F ; :: according to FILTER_0:def 13 :: thesis: q,p are_equivalence_wrt F
hence q <=> p in F ; :: according to FILTER_0:def 13 :: thesis: verum