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 by XXREAL_1:3;
assume y in P ; :: thesis: [.x,y.] c= P
then A2: y < b by XXREAL_1:3;
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 by A3, XXREAL_1:1;
then A4: a <= m by A1, XXREAL_0:2;
m <= y by A3, XXREAL_1:1;
then m < b by A2, XXREAL_0:2;
hence m in P by A4, XXREAL_1:3; :: thesis: verum

end;

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