for H being non empty RelStr st H is Heyting holds
for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y )