theorem Th69: :: WAYBEL_1:69

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