set I = the carrier of I[01];
let X be Subset of I[01]; for a being Point of I[01] st X = ].a,1.] holds
X ` = [.0,a.]
let a be Point of I[01]; ( X = ].a,1.] implies X ` = [.0,a.] )
assume A1:
X = ].a,1.]
; X ` = [.0,a.]
set Y = [.0,a.];
A2:
X ` = the carrier of I[01] \ X
by SUBSET_1:def 4;
let x be object ; TARSKI:def 3 ( not x in [.0,a.] or x in X ` )
assume A5:
x in [.0,a.]
; x in X `
then reconsider y = x as Real ;
A6:
0 <= y
by A5, XXREAL_1:1;
A7:
y <= a
by A5, XXREAL_1:1;
a <= 1
by BORSUK_1:43;
then
y <= 1
by A7, XXREAL_0:2;
then A8:
y in the carrier of I[01]
by A6, BORSUK_1:43;
not y in X
by A1, A7, XXREAL_1:2;
hence
x in X `
by A2, A8, XBOOLE_0:def 5; verum