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

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

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