let A be Subset of I[01] ; :: thesis: for a, b being real number st a < b & A = ].a,b.[ holds
[.a,b.] c= the carrier of I[01]
let a, b be real number ; :: thesis: ( a < b & A = ].a,b.[ implies [.a,b.] c= the carrier of I[01] )
assume A1: a < b ; :: thesis: ( not A = ].a,b.[ or [.a,b.] c= the carrier of I[01] )
assume A2: A = ].a,b.[ ; :: thesis: [.a,b.] c= the carrier of I[01]
then A3: 0 <= a by A1, BORSUK_1:83, XXREAL_1:51;
b <= 1 by A1, A2, BORSUK_1:83, XXREAL_1:51;
hence [.a,b.] c= the carrier of I[01] by A3, BORSUK_1:83, XXREAL_1:34; :: thesis: verum