let a, b be real number ; :: thesis: ].a,b.[ is convex Subset of R^1
reconsider P = ].a,b.[ as Subset of R^1 by TOPMETR:24;
P is convex

proof

let x, y be Point of R^1 ; :: according to TOPALG_2:def 3 :: thesis: ( x in P & y in P implies [.x,y.] c= P )
assume x in P ; :: thesis: ( not y in P or [.x,y.] c= P )
then A1: ( a < x & x < b ) by XXREAL_1:4;
assume y in P ; :: thesis: [.x,y.] c= P
then A2: ( a < y & y < b ) by XXREAL_1:4;
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in [.x,y.] or m in P )
assume A3: m in [.x,y.] ; :: thesis: m in P
then reconsider m = m as Real ;
( x <= m & m <= y ) by A3, XXREAL_1:1;
then ( a < m & m < b ) by A1, A2, XXREAL_0:2;
hence m in P by XXREAL_1:4; :: thesis: verum

end;

hence ].a,b.[ is convex Subset of R^1 ; :: thesis: verum