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