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 a "/\" b = Bottom H ) )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H holds
( 'not' a >= b iff a "/\" b = Bottom H )
let a, b be Element of H; :: thesis: ( 'not' a >= b iff a "/\" b = Bottom H )

hereby :: thesis: ( a "/\" b = Bottom H implies 'not' a >= b )

assume 'not' a >= b ; :: thesis: a "/\" b = Bottom H
then A2: a "/\" b <= Bottom H by A1, Th67;
a "/\" b >= Bottom H by A1, YELLOW_0:44;
hence a "/\" b = Bottom H by A1, A2, ORDERS_2:2; :: thesis: verum

end;

assume a "/\" b = Bottom H ; :: thesis: 'not' a >= b
then a "/\" b <= Bottom H by A1, ORDERS_2:1;
hence 'not' a >= b by A1, Th67; :: thesis: verum