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

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 & b [= b "\/" a & b "\/" a = a "\/" b & x [= x "\/" y & y [= y "\/" x & y "\/" x = x "\/" y ) by LATTICES:22;
then ( [x,xy] in LattRel L2 & [y,xy] in LattRel L2 & [a,ab] in LattRel L1 & [b,ab] in LattRel L1 ) by A1, FILTER_1:32;
then ( a [= ab & b [= ab & x [= xy & y [= xy ) by FILTER_1:32;
then A2: ( a "\/" b [= ab & x "\/" y [= xy ) by FILTER_0:6;
then [ab,(a "\/" b)] in LattRel L1 by A1, FILTER_1:32;
then ( ab [= a "\/" b & H₂(L1) . a,b = a "\/" b & j . x,y = x "\/" y ) by FILTER_1:32;
hence H₂(L1) . a,b = j . a,b by A2, LATTICES:26; :: thesis: verum

end;

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

now

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;
( a "/\" b [= a & b "/\" a [= b & b "/\" a = a "/\" b & x "/\" y [= x & y "/\" x [= y & y "/\" x = x "/\" y ) by LATTICES:23;
then ( [xy,x] in LattRel L2 & [xy,y] in LattRel L2 & [ab,a] in LattRel L1 & [ab,b] in LattRel L1 ) by A1, FILTER_1:32;
then ( ab [= a & ab [= b & xy [= x & xy [= y ) by FILTER_1:32;
then A4: ( ab [= a "/\" b & xy [= x "/\" y ) by FILTER_0:7;
then [(a "/\" b),ab] in LattRel L1 by A1, FILTER_1:32;
then ( a "/\" b [= ab & H₃(L1) . a,b = a "/\" b & m . x,y = x "/\" y ) by FILTER_1:32;
hence H₃(L1) . a,b = m . a,b by A4, LATTICES:26; :: 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, A3, BINOP_1:2; :: thesis: verum