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:22;
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