reconsider U = [.0,(2 / 3).[, V = ].(1 / 3),1.] as Subset of I[01] by BORSUK_1:40, XXREAL_1:35, XXREAL_1:36;
reconsider B = { ].a,b.[ where a, b is Real : a < b } as Basis of R^1 by Th72;
set S = I[01] ;
set T = R^1 ;
set A1 = { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } ;
set A2 = { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ;
set A3 = { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ;
set B9 = { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } ;
A1: { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } = (( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) \/ {([#] I[01])}

reconsider aa = ].(- 1),2.[ as Subset of R^1 by TOPMETR:17;
thus { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } c= (( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) \/ {([#] I[01])} :: according to XBOOLE_0:def 10 :: thesis:

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } ; :: thesis:
then consider A being Subset of R^1 such that
A2: u = A /\ ([#] I[01]) and
A3: A in B and
A4: A meets [#] I[01] ;
consider x being object such that
A5: x in A and
A6: x in [#] I[01] by A4, XBOOLE_0:3;
consider a, b being Real such that
A7: A = ].a,b.[ and
A8: a < b by A3;
reconsider x = x as Real by A5;
A9: a < x by A7, A5, XXREAL_1:4;
A10: x <= 1 by A6, BORSUK_1:40, XXREAL_1:1;
A11: 0 <= x by A6, BORSUK_1:40, XXREAL_1:1;

per cases ;

suppose A12: ( a < 0 & b <= 1 ) ; :: thesis:

A13: 0 < b by A11, A7, A5, XXREAL_1:4;
u = [.0,b.[ by A12, A2, A7, BORSUK_1:40, XXREAL_1:148;
then u in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } by A13, A12;
then u in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } by XBOOLE_0:def 3;
then u in ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ ( { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } \/ {([#] I[01])}) by XBOOLE_0:def 3;
hence u in (( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) \/ {([#] I[01])} by XBOOLE_1:4; :: thesis:

end;

suppose ( a < 0 & b > 1 ) ; :: thesis:

then u = [#] I[01] by A2, A7, BORSUK_1:40, XBOOLE_1:28, XXREAL_1:47;
hence u in (( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) \/ {([#] I[01])} by ZFMISC_1:136; :: thesis:

end;

suppose A14: ( a >= 0 & b <= 1 ) ; :: thesis:

then u = A by A2, A7, BORSUK_1:40, XBOOLE_1:28, XXREAL_1:37;
then u in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } by A7, A8, A14;
then u in ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } by XBOOLE_0:def 3;
hence u in (( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) \/ {([#] I[01])} by XBOOLE_0:def 3; :: thesis:

end;

suppose A15: ( a >= 0 & b > 1 ) ; :: thesis:

A16: a < 1 by A10, A9, XXREAL_0:2;
u = ].a,1.] by A15, A2, A7, BORSUK_1:40, XXREAL_1:149;
then u in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } by A16, A15;
then u in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } by XBOOLE_0:def 3;
then u in ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ ( { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } \/ {([#] I[01])}) by XBOOLE_0:def 3;
hence u in (( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) \/ {([#] I[01])} by XBOOLE_1:4; :: thesis:

end;

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in (( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) \/ {([#] I[01])} ; :: thesis:
then ( u in ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } or u in {([#] I[01])} ) by XBOOLE_0:def 3;
then A17: ( u in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } or u in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } or u in {([#] I[01])} ) by XBOOLE_0:def 3;

per cases by A17, XBOOLE_0:def 3;

suppose u in {([#] I[01])} ; :: thesis:

then u = [#] I[01] by TARSKI:def 1;
then A18: u = aa /\ ([#] I[01]) by BORSUK_1:40, XBOOLE_1:28, XXREAL_1:47;
[#] I[01] c= aa by BORSUK_1:40, XXREAL_1:47;
then A19: aa meets [#] I[01] by XBOOLE_1:68;
aa in B ;
hence u in { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } by A18, A19; :: thesis:

end;

suppose u in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } ; :: thesis:

then consider a being Real such that
A20: u = [.0,a.[ and
A21: 0 < a and
A22: a <= 1 ;
reconsider A = ].(- 1),a.[ as Subset of R^1 by TOPMETR:17;
A23: A in B by A21;
A24: 0 in [.0,1.] by XXREAL_1:1;
0 in A by A21, XXREAL_1:4;
then A25: A meets [#] I[01] by A24, BORSUK_1:40, XBOOLE_0:3;
u = A /\ [.0,1.] by A20, A22, XXREAL_1:148;
hence u in { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } by A23, A25, BORSUK_1:40; :: thesis:

end;

suppose u in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ; :: thesis:

then consider a being Real such that
A26: u = ].a,1.] and
A27: 0 <= a and
A28: a < 1 ;
reconsider A = ].a,2.[ as Subset of R^1 by TOPMETR:17;
2 > a by A28, XXREAL_0:2;
then A29: A in B ;
A30: 1 in [.0,1.] by XXREAL_1:1;
1 in A by A28, XXREAL_1:4;
then A31: A meets [#] I[01] by A30, BORSUK_1:40, XBOOLE_0:3;
u = A /\ [.0,1.] by A26, A27, XXREAL_1:149;
hence u in { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } by A29, A31, BORSUK_1:40; :: thesis:

end;

suppose u in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ; :: thesis:

then consider a, b being Real such that
A32: u = ].a,b.[ and
A33: 0 <= a and
A34: a < b and
A35: b <= 1 ;
reconsider A = ].a,b.[ as Subset of R^1 by TOPMETR:17;
A36: A c= [.0,1.] by A33, A35, XXREAL_1:37;
a + b < b + b by A34, XREAL_1:8;
then A37: (a + b) / 2 < (b + b) / 2 by XREAL_1:74;
a + a < a + b by A34, XREAL_1:8;
then (a + a) / 2 < (a + b) / 2 by XREAL_1:74;
then (a + b) / 2 in A by A37, XXREAL_1:4;
then A38: A meets [#] I[01] by A36, BORSUK_1:40, XBOOLE_0:3;
A39: A in B by A34;
u = A /\ [.0,1.] by A33, A35, A32, XBOOLE_1:28, XXREAL_1:37;
hence u in { (A /\ ([#] I[01])) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } by A39, A38, BORSUK_1:40; :: thesis:

end;

U in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } ;
then U in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } by XBOOLE_0:def 3;
then A40: U in ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } by XBOOLE_0:def 3;
V in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ;
then V in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } by XBOOLE_0:def 3;
then A41: V in ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } by XBOOLE_0:def 3;
U \/ V = [#] I[01] by BORSUK_1:40, XXREAL_1:175;
hence ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } is Basis of I[01] by A1, A40, A41, Th71, Th73; :: thesis: