theorem :: JORDAN1A:9

for r, s being Real holds |[r,s]| in Vertical_Line r