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] )
A2: ].a,b.[ c= ].a,b.] by XXREAL_1:21;
assume A = ].a,b.] ; :: thesis: [.a,b.] c= the carrier of I[01]
then A3: ].a,b.[ c= [.0 ,1.] by A2, BORSUK_1:83, XBOOLE_1:1;
then A4: 0 <= a by A1, XXREAL_1:51;
b <= 1 by A1, A3, XXREAL_1:51;
hence [.a,b.] c= the carrier of I[01] by A4, BORSUK_1:83, XXREAL_1:34; :: thesis: verum