theorem Th4: :: JORDAN21:4

for s, t1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t1 < t } holds
P is convex