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 ) } ;
reconsider B = { ].a,b.[ where a, b is Real : a < b } as Basis of R^1 by Th76;
set B' = { (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] )}
proof
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: (({ [.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] )} c= { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } proof
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } or 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] )} )
assume
u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) }
;
:: thesis: 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] )}
then consider A being
Subset of
R^1 such that A2:
(
u = A /\ ([#] I[01] ) &
A in B &
A meets [#] I[01] )
;
consider a,
b being
Real such that A3:
(
A = ].a,b.[ &
a < b )
by A2;
consider x being
set such that A4:
(
x in A &
x in [#] I[01] )
by A2, XBOOLE_0:3;
reconsider x =
x as
Real by A3, A4;
A5:
(
0 <= x &
x <= 1 &
a < x &
x < b )
by A3, A4, BORSUK_1:83, XXREAL_1:1, XXREAL_1:4;
per cases
( ( a < 0 & b <= 1 ) or ( a < 0 & b > 1 ) or ( a >= 0 & b <= 1 ) or ( a >= 0 & b > 1 ) )
;
suppose A6:
(
a < 0 &
b <= 1 )
;
:: thesis: 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] )}then
(
u = [.0 ,b.[ &
0 < b )
by A2, A3, A5, BORSUK_1:83, XXREAL_1:148;
then
u in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) }
by A6;
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: verum end; suppose A7:
(
a >= 0 &
b <= 1 )
;
:: thesis: 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] )}then
u = A
by A2, A3, BORSUK_1:83, XBOOLE_1:28, XXREAL_1:37;
then
u in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) }
by A3, A7;
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: verum end; suppose A8:
(
a >= 0 &
b > 1 )
;
:: thesis: 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] )}then
(
u = ].a,1.] &
a < 1 )
by A2, A3, A5, BORSUK_1:83, XXREAL_0:2, XXREAL_1:149;
then
u in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) }
by A8;
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: verum end;
end;
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not 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] )} or u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } )
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: u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) }
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 A9:
(
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;
reconsider aa =
].(- 1),2.[ as
Subset of
R^1 by TOPMETR:24;
per cases
( u in {([#] I[01] )} or u in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } or u in { ].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 ) } )
by A9, XBOOLE_0:def 3;
suppose
u in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) }
;
:: thesis: u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } then consider a being
Real such that A11:
(
u = ].a,1.] &
0 <= a &
a < 1 )
;
reconsider A =
].a,2.[ as
Subset of
R^1 by TOPMETR:24;
( 1
in [.0 ,1.] & 1
in A & 2
> a )
by A11, XXREAL_0:2, XXREAL_1:1, XXREAL_1:4;
then
(
u = A /\ [.0 ,1.] &
A in B &
A meets [#] I[01] )
by A11, BORSUK_1:83, XBOOLE_0:3, XXREAL_1:149;
hence
u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) }
by BORSUK_1:83;
:: thesis: verum end; suppose
u in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) }
;
:: thesis: u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) } then consider a,
b being
Real such that A12:
(
u = ].a,b.[ &
0 <= a &
a < b &
b <= 1 )
;
reconsider A =
].a,b.[ as
Subset of
R^1 by TOPMETR:24;
(
a + a < a + b &
a + b < b + b )
by A12, XREAL_1:10;
then
(
(a + a) / 2
< (a + b) / 2 &
(a + b) / 2
< (b + b) / 2 )
by XREAL_1:76;
then A13:
(a + b) / 2
in A
by XXREAL_1:4;
A c= [.0 ,1.]
by A12, XXREAL_1:37;
then
(
u = A /\ [.0 ,1.] &
A in B &
A meets [#] I[01] )
by A12, A13, BORSUK_1:83, XBOOLE_0:3, XBOOLE_1:28;
hence
u in { (A /\ ([#] I[01] )) where A is Subset of R^1 : ( A in B & A meets [#] I[01] ) }
by BORSUK_1:83;
:: thesis: verum end;
end;
reconsider U = [.0 ,(2 / 3).[, V = ].(1 / 3),1.] as Subset of I[01] by BORSUK_1:83, XXREAL_1:35, XXREAL_1:36;
( U in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } & V in { ].a,1.] 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 ) } & 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 A14:
( 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 ) } & 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:83, 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, A14, Th75, Th77; :: thesis: verum