for H being non empty RelStr st H is Heyting & H is lower-bounded holds
for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }