for a being Real
for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } holds
P is convex