let A be Subset of I[01]; :: thesis: for a, b being Real st a < b & A = ].a,b.[ holds
[.a,b.] c= the carrier of I[01]
let a, b be Real; :: 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: b <= 1 by A1, BORSUK_1:40, XXREAL_1:51;
0 <= a by A1, A2, BORSUK_1:40, XXREAL_1:51;
hence [.a,b.] c= the carrier of I[01] by A3, BORSUK_1:40, XXREAL_1:34; :: thesis: verum