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