let T be non empty convex SubSpace of R^1 ; :: thesis: for a, b being Point of T holds [.a,b.] c= the carrier of T
let a, b be Point of T; :: thesis: [.a,b.] c= the carrier of T
reconsider a1 = a, b1 = b as Point of R^1 by PRE_TOPC:55;
[#] T is convex Subset of R^1 by Def4;
then [.a1,b1.] c= the carrier of T by Def3;
hence [.a,b.] c= the carrier of T ; :: thesis: verum