let L1, L2 be Lattice; ( 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
; 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 = H2(L2), m = H3(L2) as BinOp of H1(L1) by A1;
now for a, b being Element of L1 holds H2(L1) . (a,b) = j . (a,b)let a,
b be
Element of
L1;
H2(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
H2(
L1)
. (
a,
b)
= j . (
a,
b)
by A14, LATTICES:8;
verum end;
then A15:
H2(L1) = j
by BINOP_1:2;
now for a, b being Element of L1 holds H3(L1) . (a,b) = m . (a,b)let a,
b be
Element of
L1;
H3(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
H3(
L1)
. (
a,
b)
= m . (
a,
b)
by A28, LATTICES:8;
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; verum