for T being non empty lower TopRelStr
for x being Point of T holds
( (uparrow x) ` is open & uparrow x is closed )