set I = the carrier of I[01];
let X be Subset of I[01]; :: thesis: for a being Point of I[01] st X = ].a,1.] holds
X ` = [.0,a.]
let a be Point of I[01]; :: thesis: ( X = ].a,1.] implies X ` = [.0,a.] )
assume A1: X = ].a,1.] ; :: thesis: X ` = [.0,a.]
set Y = [.0,a.];
A2: X ` = the carrier of I[01] \ X by SUBSET_1:def 4;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [.0,a.] c= X `
let x be object ; :: thesis: ( x in X ` implies x in [.0,a.] )
assume A3: x in X ` ; :: thesis: x in [.0,a.]
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 > 1 ) by A1, XXREAL_1:2;
0 <= y by BORSUK_1:43;
hence x in [.0,a.] by A4, BORSUK_1:43, XXREAL_1:1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.0,a.] or x in X ` )
assume A5: x in [.0,a.] ; :: thesis: 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; :: thesis: verum