let L be Lattice; :: thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_reflexive_in the carrier of L
let F be Filter of L; :: thesis: ( L is I_Lattice implies equivalence_wrt F is_reflexive_in the carrier of L )
assume A1: L is I_Lattice ; :: thesis: equivalence_wrt F is_reflexive_in the carrier of L
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in the carrier of L or [x,x] in equivalence_wrt F )
assume x in the carrier of L ; :: thesis: [x,x] in equivalence_wrt F
then reconsider p = x as Element of L ;
p => p = Top L by A1, Th28;
then p <=> p = Top L ;
then p <=> p in F by A1, Th11;
hence [x,x] in equivalence_wrt F by Def11; :: thesis: verum