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 be set ; :: according to RELAT_2:def 3 :: thesis: for b₁ being set holds
( not x in the carrier of L or not b₁ in the carrier of L or not [x,b₁] in equivalence_wrt F or [b₁,x] in equivalence_wrt F )
let y be set ; :: 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 Def12;
then q <=> p in F ;
hence [y,x] in equivalence_wrt F by Def12; :: thesis: verum