let a, b be Point of I[01] ; :: thesis: ( a < b & b <> 1 implies ].a,b.] is non empty Subset of I(01) )
assume A1: ( a < b & b <> 1 ) ; :: thesis: ].a,b.] is non empty Subset of I(01)
( 0 <= a & b <= 1 ) by BORSUK_1:86;
then A2: b < 1 by A1, XXREAL_0:1;
].a,b.] c= the carrier of I(01)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].a,b.] or x in the carrier of I(01) )
assume x in ].a,b.] ; :: thesis: x in the carrier of I(01)
then x in { r where r is Real : ( a < r & r <= b ) } by RCOMP_1:def 9;
then consider r being Real such that
A3: ( x = r & a < r & r <= b ) ;
( 0 < r & r < 1 ) by A2, A3, BORSUK_1:86, XXREAL_0:2;
hence x in the carrier of I(01) by A3, Th60; :: thesis: verum

end;

hence ].a,b.] is non empty Subset of I(01) by A1, XXREAL_1:2; :: thesis: verum