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: 'not' b >= 'not' b by A1, ORDERS_2:1;
assume a <= b ; :: thesis: 'not' b <= 'not' a
then a "/\" ('not' b) = (a "/\" b) "/\" ('not' b) by A1, YELLOW_0:25
.= a "/\" (b "/\" ('not' b)) by A1, LATTICE3:16
.= a "/\" (Bottom H) by A1, A2, Th82
.= (Bottom H) "/\" a by A1, LATTICE3:15
.= Bottom H by A1, Th3 ;
hence 'not' b <= 'not' a by A1, Th82; :: thesis: verum