let T be non empty interval 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:25;
[#] T is interval Subset of T by Def3;
then [.a1,b1.] c= the carrier of T by XXREAL_2:def 12;
hence [.a,b.] c= the carrier of T ; :: thesis: verum