let a, b be Point of I[01] ; :: thesis: ( a < b & a <> 0 implies [.a,b.[ is non empty Subset of I(01) )
assume A1: ( a < b & a <> 0 ) ; :: thesis: [.a,b.[ is non empty Subset of I(01)
A2: ( 0 <= a & b <= 1 ) by BORSUK_1:86;
[.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 8;
then consider r being Real such that
A3: ( x = r & a <= r & r < b ) ;
( 0 < r & r < 1 ) by A1, A2, A3, 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:3; :: thesis: verum