reconsider I = L as I_Lattice by A1;

reconsider FI = F as Filter of I ;

set R = equivalence_wrt FI;

reconsider o1 = H_{1}(L), o2 = H_{2}(L) as BinOp of equivalence_wrt FI by Th13, Th14;

let L1, L2 be strict Lattice; :: thesis: ( ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

L1 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

L2 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) implies L1 = L2 )

assume that

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

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

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

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

thus L1 = LattStr(# (Class (equivalence_wrt FI)),(o1 /\/ (equivalence_wrt FI)),(o2 /\/ (equivalence_wrt FI)) #) by A7

.= L2 by A8 ; :: thesis: verum

reconsider FI = F as Filter of I ;

set R = equivalence_wrt FI;

reconsider o1 = H

let L1, L2 be strict Lattice; :: thesis: ( ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

L1 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

L2 = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) implies L1 = L2 )

assume that

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

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

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

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

thus L1 = LattStr(# (Class (equivalence_wrt FI)),(o1 /\/ (equivalence_wrt FI)),(o2 /\/ (equivalence_wrt FI)) #) by A7

.= L2 by A8 ; :: thesis: verum