REAL c= the carrier of R^1 by TOPMETR:24;
then reconsider P = REAL as non empty Subset of R^1 ;
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 R^1 ; :: 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