theorem Th5: :: WAYBEL19:5

for T being non empty transitive lower TopRelStr
for A being Subset of T st A is open holds
A is lower