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
then A2: H is LATTICE ;
let a, b, c be Element of H; :: thesis: ( b <= c implies a => b <= a => c )
assume A3: b <= c ; :: thesis: a => b <= a => c
a "/\" (a => b) <= b by A1, Lm5;
then a "/\" (a => b) <= c by A2, A3, ORDERS_2:26;
hence a => b <= a => c by A1, Th70; :: thesis: verum