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 )
consider o1, o2 being BinOp of F1 such that
A1: ( o1 = the L_join of L1 || F1 & o2 = the L_meet of L1 || F1 & latt F1 = LattStr(# F1,o1,o2 #) ) by FILTER_0:def 10;
consider p1, p2 being BinOp of F2 such that
A2: ( p1 = the L_join of L2 || F2 & p2 = the L_meet of L2 || F2 & latt F2 = LattStr(# F2,p1,p2 #) ) by FILTER_0:def 10;
thus ( 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 A1, A2; :: thesis: verum