let L1, L2 be WA_Lattice; :: thesis: ( LatRelStr L1 = LatRelStr 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: LatRelStr L1 = LatRelStr 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 = the L_join of L2, m = the L_meet of L2 as BinOp of the carrier of 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;
a [= a "\/" b by LATWAL_1:9;
then A6: [x,xy] in LatOrder L2 by A1;
b [= b "\/" a by LATWAL_1:9;
then A7: [y,xy] in LatOrder L2 by A1;
x [= x "\/" y by LATWAL_1:9;
then A8: [a,ab] in LatOrder L1 by A1;
y [= y "\/" x by LATWAL_1:9;
then A9: [b,ab] in LatOrder L1 by A1;
A10: a [= ab by A8, Idem2;
A11: b [= ab by A9, Idem2;
A12: x [= xy by A6, Idem2;
A13: y [= xy by A7, Idem2;
A14: a "\/" b [= ab by A10, A11, LATWAL_1:11;
x "\/" y [= xy by A12, A13, LATWAL_1:11;
then [ab,(a "\/" b)] in LatOrder L1 by A1;
then ab [= a "\/" b by Idem2;
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;
x "/\" y [= x by LATTICES:6;
then [ab,a] in LatOrder L1 by A1;
then A24: ab [= a by Idem2;
y "/\" x [= y by LATTICES:6;
then [ab,b] in LatOrder L1 by A1;
then A25: ab [= b by Idem2;
a "/\" b [= a by LATTICES:6;
then [xy,x] in LatOrder L2 by A1;
then A26: xy [= x by Idem2;
b "/\" a [= b by LATTICES:6;
then [xy,y] in LatOrder L2 by A1;
then A27: xy [= y by Idem2;
A28: ab [= a "/\" b by A24, A25, LATWAL_1:13;
xy [= x "/\" y by A26, A27, LATWAL_1:13;
then [(a "/\" b),ab] in LatOrder L1 by A1;
then a "/\" b [= ab by Idem2;
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