let L1, L2 be Lattice; :: thesis: for F1 being Filter of L1
for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds
latt F1 = latt F2
let F1 be Filter of L1; :: thesis: for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds
latt F1 = latt F2
let F2 be Filter of L2; :: thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 implies latt F1 = latt F2 )
ex o1, o2 being BinOp of F1 st
( o1 = the L_join of L1 || F1 & o2 = the L_meet of L1 || F1 & latt F1 = LattStr(# F1,o1,o2 #) ) by FILTER_0:def 9;
hence ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 implies latt F1 = latt F2 ) by FILTER_0:def 9; :: thesis: verum