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