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