let L1, L2 be Lattice; :: thesis: ( LattPOSet L1 = LattPOSet L2 implies 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 #) )
assume A1: LattPOSet L1 = LattPOSet 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 #)
reconsider j = H₂(L2), m = H₃(L2) as BinOp of H₁(L1) by A1;

now :: thesis: for a, b being Element of L1 holds H₂(L1) . (a,b) = j . (a,b)

let a, b be Element of L1; :: thesis: H₂(L1) . (a,b) = j . (a,b)
reconsider x = a, y = b, xy = a "\/" b as Element of L2 by A1;
reconsider ab = x "\/" y as Element of L1 by A1;
A2: a [= a "\/" b by LATTICES:5;
A3: b [= b "\/" a by LATTICES:5;
A4: x [= x "\/" y by LATTICES:5;
A5: y [= y "\/" x by LATTICES:5;
A6: [x,xy] in LattRel L2 by A1, A2, FILTER_1:31;
A7: [y,xy] in LattRel L2 by A1, A3, FILTER_1:31;
A8: [a,ab] in LattRel L1 by A1, A4, FILTER_1:31;
A9: [b,ab] in LattRel L1 by A1, A5, FILTER_1:31;
A10: a [= ab by A8, FILTER_1:31;
A11: b [= ab by A9, FILTER_1:31;
A12: x [= xy by A6, FILTER_1:31;
A13: y [= xy by A7, FILTER_1:31;
A14: a "\/" b [= ab by A10, A11, FILTER_0:6;
x "\/" y [= xy by A12, A13, FILTER_0:6;
then [ab,(a "\/" b)] in LattRel L1 by A1, FILTER_1:31;
then ab [= a "\/" b by FILTER_1:31;
hence H₂(L1) . (a,b) = j . (a,b) by A14, LATTICES:8; :: thesis: verum

end;

then A15: H₂(L1) = j by BINOP_1:2;

now :: thesis: for a, b being Element of L1 holds H₃(L1) . (a,b) = m . (a,b)

let a, b be Element of L1; :: thesis: H₃(L1) . (a,b) = m . (a,b)
reconsider x = a, y = b, xy = a "/\" b as Element of L2 by A1;
reconsider ab = x "/\" y as Element of L1 by A1;
A16: a "/\" b [= a by LATTICES:6;
A17: b "/\" a [= b by LATTICES:6;
A18: x "/\" y [= x by LATTICES:6;
A19: y "/\" x [= y by LATTICES:6;
A20: [xy,x] in LattRel L2 by A1, A16, FILTER_1:31;
A21: [xy,y] in LattRel L2 by A1, A17, FILTER_1:31;
A22: [ab,a] in LattRel L1 by A1, A18, FILTER_1:31;
A23: [ab,b] in LattRel L1 by A1, A19, FILTER_1:31;
A24: ab [= a by A22, FILTER_1:31;
A25: ab [= b by A23, FILTER_1:31;
A26: xy [= x by A20, FILTER_1:31;
A27: xy [= y by A21, FILTER_1:31;
A28: ab [= a "/\" b by A24, A25, FILTER_0:7;
xy [= x "/\" y by A26, A27, FILTER_0:7;
then [(a "/\" b),ab] in LattRel L1 by A1, FILTER_1:31;
then a "/\" b [= ab by FILTER_1:31;
hence H₃(L1) . (a,b) = m . (a,b) by A28, LATTICES:8; :: thesis: verum

end;

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 #) by A1, A15, BINOP_1:2; :: thesis: verum