for H being non empty RelStr st H is Heyting holds
H is upper-bounded