for H being non empty RelStr st H is Heyting & H is lower-bounded holds
( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H )