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

proof

let x be object ; :: 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 8;
then consider r being Real such that
A4: x = r and
A5: a < r and
A6: r <= b ;
A7: 0 < r by A5, BORSUK_1:43;
r < 1 by A3, A6, XXREAL_0:2;
hence x in the carrier of I(01) by A4, A7, Th32; :: thesis: verum

end;

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