reconsider I = L as I_Lattice by A1;
reconsider FI = F as Filter of I ;
set R = equivalence_wrt FI;
reconsider j = H₁(I), m = H₂(I) as BinOp of equivalence_wrt FI by Th13, Th14;
reconsider i = a as Element of I ;
I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),(j /\/ (equivalence_wrt FI)),(m /\/ (equivalence_wrt FI)) #) by Def5;
then reconsider c = EqClass (equivalence_wrt FI),i as Element of (L /\/ F) ;
take c ; :: thesis: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
c = Class R,a
thus for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
c = Class R,a ; :: thesis: verum