theorem :: WAYBEL_1:73

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