REAL c= the carrier of R^1 by TOPMETR:24;
then reconsider P = REAL as non empty Subset of ;
take P ; :: thesis: ( not P is empty & P is convex )
thus not P is empty ; :: thesis: P is convex
let a, b be Point of ; :: according to TOPALG_2:def 3 :: thesis: ( a in P & b in P implies [.a,b.] c= P )
thus ( a in P & b in P implies [.a,b.] c= P ) ; :: thesis: verum