set I = the carrier of I[01];
let X be Subset of I[01]; :: thesis: for a being Point of I[01] st X = [.0,a.[ holds
X ` = [.a,1.]
let a be Point of I[01]; :: thesis: ( X = [.0,a.[ implies X ` = [.a,1.] )
assume A1: X = [.0,a.[ ; :: thesis: X ` = [.a,1.]
set Y = [.a,1.];
A2: X ` = the carrier of I[01] \ X by SUBSET_1:def 4;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [.a,1.] c= X `

let x be object ; :: thesis: ( x in X ` implies x in [.a,1.] )
assume A3: x in X ` ; :: thesis: x in [.a,1.]
then reconsider y = x as Point of I[01] ;
not x in X by A2, A3, XBOOLE_0:def 5;
then A4: ( y >= a or y < 0 ) by A1, XXREAL_1:3;
y <= 1 by BORSUK_1:43;
hence x in [.a,1.] by A4, BORSUK_1:43, XXREAL_1:1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.a,1.] or x in X ` )
assume A5: x in [.a,1.] ; :: thesis: x in X `
then reconsider y = x as Real ;
A6: a <= y by A5, XXREAL_1:1;
then A7: not y in X by A1, XXREAL_1:3;
A8: 0 <= a by BORSUK_1:43;
y <= 1 by A5, XXREAL_1:1;
then y in the carrier of I[01] by A6, A8, BORSUK_1:43;
hence x in X ` by A2, A7, XBOOLE_0:def 5; :: thesis: verum