let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H holds a "/\" (a => b) <= b )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H holds a "/\" (a => b) <= b
let a, b be Element of H; :: thesis: a "/\" (a => b) <= b
a => b <= a => b by A1, ORDERS_2:1;
hence a "/\" (a => b) <= b by A1, Th67; :: thesis: verum