reconsider I = L as I_Lattice by A1;

reconsider FI = F as Filter of I ;

set R = equivalence_wrt FI;

reconsider j = H_{1}(I), m = H_{2}(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

reconsider FI = F as Filter of I ;

set R = equivalence_wrt FI;

reconsider j = H

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