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])}
proof
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])}
XBOOLE_0:def 10 (( { [.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
object ;
TARSKI:def 3 ( 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] ) }
;
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])
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
( ( a < 0 & b <= 1 ) or ( a < 0 & b > 1 ) or ( a >= 0 & b <= 1 ) or ( a >= 0 & b > 1 ) )
;
suppose A12:
(
a < 0 &
b <= 1 )
;
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])}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;
verum end; suppose A14:
(
a >= 0 &
b <= 1 )
;
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, 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;
verum end; suppose A15:
(
a >= 0 &
b > 1 )
;
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])}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;
verum end;
end;
let u be
object ;
TARSKI:def 3 ( 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])}
;
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 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
( 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 A17, XBOOLE_0:def 3;
suppose
u in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) }
;
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 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;
verum end; suppose
u in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) }
;
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 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;
verum end; suppose
u in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) }
;
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 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;
verum end;
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; verum