set I = the carrier of I[01];
let X be Subset of I[01]; for a being Point of I[01] st X = [.0,a.[ holds
X ` = [.a,1.]
let a be Point of I[01]; ( X = [.0,a.[ implies X ` = [.a,1.] )
assume A1:
X = [.0,a.[
; X ` = [.a,1.]
set Y = [.a,1.];
A2:
X ` = the carrier of I[01] \ X
by SUBSET_1:def 4;
let x be object ; TARSKI:def 3 ( not x in [.a,1.] or x in X ` )
assume A5:
x in [.a,1.]
; 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; verum