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 & ( for Y, Z being Subset of X holds
( H₂(L1) . Y,Z = Y \/ Z & H₃(L1) . Y,Z = Y /\ Z ) ) ) and
A4: ( the carrier of L2 = bool X & ( 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, A4;

now

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

end;

then A5: j1 = j2 by BINOP_1:2;

now

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

end;

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