let L1, L2 be strict LattStr ; :: thesis: ( 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
( H₂(L1) . (Y,Z) = Y \/ Z & H₃(L1) . (Y,Z) = Y /\ Z ) and
A5: the carrier of L2 = bool X and
A6: for Y, Z being Subset of X holds
( H₂(L2) . (Y,Z) = Y \/ Z & H₃(L2) . (Y,Z) = Y /\ Z ) ; :: thesis: L1 = L2
reconsider j1 = H₂(L1), j2 = H₂(L2), m1 = H₃(L1), m2 = H₃(L2) as BinOp of (bool X) by A3, A5;

now :: thesis: for x, y being Subset of X holds j1 . (x,y) = j2 . (x,y)

let x, y be Subset of X; :: thesis: j1 . (x,y) = j2 . (x,y)
thus j1 . (x,y) = x \/ y by A4
.= j2 . (x,y) by A6 ; :: thesis: verum

end;

then A7: j1 = j2 by BINOP_1:2;

now :: thesis: for x, y being Subset of X holds m1 . (x,y) = m2 . (x,y)

let x, y be Subset of X; :: thesis: m1 . (x,y) = m2 . (x,y)
thus m1 . (x,y) = x /\ y by A4
.= m2 . (x,y) by A6 ; :: thesis: verum

end;

hence L1 = L2 by A3, A5, A7, BINOP_1:2; :: thesis: verum