let A be Subset of I[01]; for a, b being Real st a <= b & A = [.a,b.] holds
( 0 <= a & b <= 1 )
let a, b be Real; ( a <= b & A = [.a,b.] implies ( 0 <= a & b <= 1 ) )
assume that
A1:
a <= b
and
A2:
A = [.a,b.]
; ( 0 <= a & b <= 1 )
A3:
b in A
by A1, A2, XXREAL_1:1;
a in A
by A1, A2, XXREAL_1:1;
hence
( 0 <= a & b <= 1 )
by A3, BORSUK_1:43; verum