let L1, L2 be strict LattStr ; ( the carrier of L1 = bool X & ( for Y, Z being Subset of X holds
( the L_join of L1 . (Y,Z) = Y \/ Z & the L_meet of L1 . (Y,Z) = Y /\ Z ) ) & the carrier of L2 = bool X & ( for Y, Z being Subset of X holds
( the L_join of L2 . (Y,Z) = Y \/ Z & the L_meet of L2 . (Y,Z) = Y /\ Z ) ) implies L1 = L2 )
assume that
A3:
the carrier of L1 = bool X
and
A4:
for Y, Z being Subset of X holds
( H2(L1) . (Y,Z) = Y \/ Z & H3(L1) . (Y,Z) = Y /\ Z )
and
A5:
the carrier of L2 = bool X
and
A6:
for Y, Z being Subset of X holds
( H2(L2) . (Y,Z) = Y \/ Z & H3(L2) . (Y,Z) = Y /\ Z )
; L1 = L2
reconsider j1 = H2(L1), j2 = H2(L2), m1 = H3(L1), m2 = H3(L2) as BinOp of (bool X) by A3, A5;
now for x, y being Subset of X holds j1 . (x,y) = j2 . (x,y)let x,
y be
Subset of
X;
j1 . (x,y) = j2 . (x,y)thus j1 . (
x,
y) =
x \/ y
by A4
.=
j2 . (
x,
y)
by A6
;
verum end;
then A7:
j1 = j2
by BINOP_1:2;
now for x, y being Subset of X holds m1 . (x,y) = m2 . (x,y)let x,
y be
Subset of
X;
m1 . (x,y) = m2 . (x,y)thus m1 . (
x,
y) =
x /\ y
by A4
.=
m2 . (
x,
y)
by A6
;
verum end;
hence
L1 = L2
by A3, A5, A7, BINOP_1:2; verum