let H be non empty lower-bounded RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H st a <= b holds
'not' b <= 'not' a )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H st a <= b holds
'not' b <= 'not' a
let a, b be Element of H; :: thesis: ( a <= b implies 'not' b <= 'not' a )
A2: H is LATTICE by A1;
then A3: 'not' b >= 'not' b by ORDERS_2:24;
assume a <= b ; :: thesis: 'not' b <= 'not' a
then a "/\" ('not' b) = (a "/\" b) "/\" ('not' b) by A2, YELLOW_0:25
.= a "/\" (b "/\" ('not' b)) by A2, LATTICE3:16
.= a "/\" (Bottom H) by A1, A3, Th85
.= (Bottom H) "/\" a by A2, LATTICE3:15
.= Bottom H by A2, Th4 ;
hence 'not' b <= 'not' a by A1, Th85; :: thesis: verum