let L be Lattice; :: thesis: for F being Filter of L st L is I_Lattice holds
field (equivalence_wrt F) = the carrier of L
let F be Filter of L; :: thesis: ( L is I_Lattice implies field (equivalence_wrt F) = the carrier of L )
assume L is I_Lattice ; :: thesis: field (equivalence_wrt F) = the carrier of L
then equivalence_wrt F is Equivalence_Relation of the carrier of L by Th67;
hence field (equivalence_wrt F) = the carrier of L by ORDERS_1:12; :: thesis: verum