let H be non empty lower-bounded RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H holds
( 'not' a >= b iff 'not' b >= a ) )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H holds
( 'not' a >= b iff 'not' b >= a )
let a, b be Element of H; :: thesis: ( 'not' a >= b iff 'not' b >= a )
A2: ( Bottom H >= a "/\" b iff a => (Bottom H) >= b ) by A1, Th67;
( Bottom H >= b "/\" a iff b => (Bottom H) >= a ) by A1, Th67;
hence ( 'not' a >= b iff 'not' b >= a ) by A1, A2, LATTICE3:15; :: thesis: verum