for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds b <= a => b