let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H holds a "/\" (a => b) = a "/\" b )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H holds a "/\" (a => b) = a "/\" b
let a, b be Element of H; :: thesis: 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; :: thesis: verum