reconsider I = L as I_Lattice by A1;
reconsider FI = F as Filter of I ;
set R = equivalence_wrt FI;
reconsider o1 = H₁(L), o2 = H₂(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