let H be non empty RelStr ; ( 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
; for a, b, c being Element of H st b <= c holds
a => b <= a => c
let a, b, c be Element of H; ( b <= c implies a => b <= a => c )
assume A2:
b <= c
; 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; verum