reconsider I = L as I_Lattice by A1;

reconsider FI = F as Filter of I ;

reconsider j = the L_join of I, m = the L_meet of I as BinOp of equivalence_wrt FI by Th13, Th14;

reconsider LL = LattStr(# (Class (equivalence_wrt FI)),(j /\/ (equivalence_wrt FI)),(m /\/ (equivalence_wrt FI)) #) as non empty strict LattStr ;

A2: H_{1}(LL) is commutative
by Th4;

A3: H_{1}(LL) is associative
by Th5;

A4: H_{2}(LL) is associative
by Th5;

A5: H_{2}(LL) is commutative
by Th4;

A6: H_{2}(LL) absorbs H_{1}(LL)
by Th12, LATTICE2:27;

H_{1}(LL) absorbs H_{2}(LL)
by Th12, LATTICE2:26;

then reconsider LL = LL as strict Lattice by A2, A3, A5, A4, A6, LATTICE2:11;

take LL ; :: thesis: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

LL = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #)

thus for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

LL = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ; :: thesis: verum

reconsider FI = F as Filter of I ;

reconsider j = the L_join of I, m = the L_meet of I as BinOp of equivalence_wrt FI by Th13, Th14;

reconsider LL = LattStr(# (Class (equivalence_wrt FI)),(j /\/ (equivalence_wrt FI)),(m /\/ (equivalence_wrt FI)) #) as non empty strict LattStr ;

A2: H

A3: H

A4: H

A5: H

A6: H

H

then reconsider LL = LL as strict Lattice by A2, A3, A5, A4, A6, LATTICE2:11;

take LL ; :: thesis: for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

LL = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #)

thus for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

LL = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ; :: thesis: verum