let T be SubSpace of R^1 ; :: thesis: ( T = R^1 implies T is convex )
assume A1: T = R^1 ; :: thesis: T is convex
reconsider P = [#] T as Subset of R^1 by A1;
P is convex

proof

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 ) by A1, TOPMETR:24; :: thesis: verum

end;

hence [#] T is convex Subset of R^1 ; :: according to TOPALG_2:def 4 :: thesis: verum