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