theorem :: JORDAN1A:10
for s being Real
for A being Subset of (TOP-REAL 2) st A c= Vertical_Line s holds
A is vertical