let L be Lattice; :: thesis: for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L
let F be Filter of L; :: thesis: equivalence_wrt F is_symmetric_in the carrier of L
let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F )
assume ( x in the carrier of L & y in the carrier of L ) ; :: thesis: ( not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F )
then reconsider p = x, q = y as Element of L ;
assume [x,y] in equivalence_wrt F ; :: thesis: [y,x] in equivalence_wrt F
then p <=> q in F by Def11;
then q <=> p in F ;
hence [y,x] in equivalence_wrt F by Def11; :: thesis: verum