theorem :: WAYBEL19:13

for T being non empty TopSpace-like reflexive transitive lower TopRelStr
for x being Point of T holds Cl {x} = uparrow x