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
then A2: H is LATTICE ;
let a, b be Element of H; :: thesis: a "/\" (a => b) = a "/\" b
(a "/\" (a => b)) "/\" a <= b "/\" a by A1, Lm5, Th2;
then a "/\" (a "/\" (a => b)) <= b "/\" a by A2, LATTICE3:15;
then a "/\" (a "/\" (a => b)) <= a "/\" b by A2, LATTICE3:15;
then (a "/\" a) "/\" (a => b) <= a "/\" b by A2, LATTICE3:16;
then A3: a "/\" (a => b) <= a "/\" b by A2, YELLOW_0:25;
b "/\" a <= (a => b) "/\" a by A1, Th2, Th75;
then a "/\" b <= (a => b) "/\" a by A2, LATTICE3:15;
then a "/\" b <= a "/\" (a => b) by A2, LATTICE3:15;
hence a "/\" (a => b) = a "/\" b by A2, A3, ORDERS_2:25; :: thesis: verum