theorem Th9: :: JORDAN1:11

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