let A be Subset of I[01] ; :: thesis: for a, b being real number st a <= b & A = [.a,b.] holds
( 0 <= a & b <= 1 )
let a, b be real number ; :: thesis: ( a <= b & A = [.a,b.] implies ( 0 <= a & b <= 1 ) )
assume ( a <= b & A = [.a,b.] ) ; :: thesis: ( 0 <= a & b <= 1 )
then ( a in A & b in A ) by XXREAL_1:1;
hence ( 0 <= a & b <= 1 ) by BORSUK_1:86; :: thesis: verum