let H be non empty RelStr ; ( H is Heyting implies for a, b being Element of H holds a "/\" (a => b) = a "/\" b )
assume A1:
H is Heyting
; for a, b being Element of H holds a "/\" (a => b) = a "/\" b
let a, b be Element of H; a "/\" (a => b) = a "/\" b
(a "/\" (a => b)) "/\" a <= b "/\" a
by A1, Lm5, Th1;
then
a "/\" (a "/\" (a => b)) <= b "/\" a
by A1, LATTICE3:15;
then
a "/\" (a "/\" (a => b)) <= a "/\" b
by A1, LATTICE3:15;
then
(a "/\" a) "/\" (a => b) <= a "/\" b
by A1, LATTICE3:16;
then A2:
a "/\" (a => b) <= a "/\" b
by A1, YELLOW_0:25;
b "/\" a <= (a => b) "/\" a
by A1, Th1, Th72;
then
a "/\" b <= (a => b) "/\" a
by A1, LATTICE3:15;
then
a "/\" b <= a "/\" (a => b)
by A1, LATTICE3:15;
hence
a "/\" (a => b) = a "/\" b
by A1, A2, ORDERS_2:2; verum