:: URYSOHN2 semantic presentation

begin

theorem Th1: :: URYSOHN2:1
for A being Subset of REAL
for x being Real st x <> 0 holds
(x ") ** (x ** A) = A
proof
let A be Subset of REAL; ::_thesis: for x being Real st x <> 0 holds
(x ") ** (x ** A) = A
let x be Real; ::_thesis: ( x <> 0 implies (x ") ** (x ** A) = A )
assume A1: x <> 0 ; ::_thesis: (x ") ** (x ** A) = A
thus  (x ") ** (x ** A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= (x ") ** (x ** A)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (x ") ** (x ** A) or y in A )
assume A2: y in (x ") ** (x ** A) ; ::_thesis: y in A
then reconsider y = y as Real ;
consider z being Real such that
A3: z in x ** A and
A4: y = (x ") * z by A2, INTEGRA2:39;
consider t being Real such that
A5: t in A and
A6: z = x * t by A3, INTEGRA2:39;
y = ((x ") * x) * t by A4, A6
.= 1 * t by A1, XCMPLX_0:def_7
.= t ;
hence  y in A by A5; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in (x ") ** (x ** A) )
assume A7: y in A ; ::_thesis: y in (x ") ** (x ** A)
then reconsider y = y as Real ;
set t = y / (x ");
A8: y / (x ") in x ** A by A7, MEMBER_1:193;
 y = (x ") * (y / (x ")) by A1, XCMPLX_1:87, XCMPLX_1:202;
hence  y in (x ") ** (x ** A) by A8, MEMBER_1:193; ::_thesis: verum
end;

theorem Th2: :: URYSOHN2:2
for x being Real st x <> 0 holds
for A being Subset of REAL st A = REAL holds
x ** A = A
proof
let x be Real; ::_thesis: ( x <> 0 implies for A being Subset of REAL st A = REAL holds
x ** A = A )
assume A1: x <> 0 ; ::_thesis: for A being Subset of REAL st A = REAL holds
x ** A = A
let A be Subset of REAL; ::_thesis: ( A = REAL implies x ** A = A )
assume A2: A = REAL ; ::_thesis: x ** A = A
 for y being set st y in A holds
y in x ** A
proof
let y be set ; ::_thesis: ( y in A implies y in x ** A )
assume  y in A ; ::_thesis: y in x ** A
then reconsider y = y as Real ;
reconsider z = y / x as Real ;
 y = x * z by A1, XCMPLX_1:87;
hence  y in x ** A by A2, MEMBER_1:193; ::_thesis: verum
end;
then  A c= x ** A by TARSKI:def_3;
hence  x ** A = A by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th3: :: URYSOHN2:3
for A being Subset of REAL st A <> {} holds
0 ** A = {0}
proof
let A be Subset of REAL; ::_thesis: ( A <> {} implies 0 ** A = {0} )
assume A1: A <> {} ; ::_thesis: 0 ** A = {0}
A2: {0} c= 0 ** A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {0} or y in 0 ** A )
consider t being set  such that
A3: t in A by A1, XBOOLE_0:def_1;
reconsider t = t as Element of A by A3;
reconsider t = t as Real by A3;
assume  y in {0} ; ::_thesis: y in 0 ** A
then  y = 0 * t by TARSKI:def_1;
hence  y in 0 ** A by A3, MEMBER_1:193; ::_thesis: verum
end;
 0 ** A c= {0}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in 0 ** A or y in {0} )
assume A4: y in 0 ** A ; ::_thesis: y in {0}
then reconsider y = y as Real ;
 ex z being Real st
( z in A & y = 0 * z ) by A4, INTEGRA2:39;
hence  y in {0} by TARSKI:def_1; ::_thesis: verum
end;
hence  0 ** A = {0} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: URYSOHN2:4
for x being Real holds x ** {} = {} ;

theorem Th5: :: URYSOHN2:5
for a, b being R_eal holds
( not a <= b or ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) )
proof
let a, b be R_eal; ::_thesis: ( not a <= b or ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) )
 ( a in REAL or a in {-infty,+infty} ) by XBOOLE_0:def_3, XXREAL_0:def_4;
then A1: ( a in REAL or a = -infty or a = +infty ) by TARSKI:def_2;
 ( b in REAL or b in {-infty,+infty} ) by XBOOLE_0:def_3, XXREAL_0:def_4;
then A2: ( b in REAL or b = -infty or b = +infty ) by TARSKI:def_2;
assume  a <= b ; ::_thesis: ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) )
hence  ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A1, A2, XXREAL_0:9, XXREAL_0:12; ::_thesis: verum
end;

theorem Th6: :: URYSOHN2:6
for A being Interval holds 0 ** A is interval
proof
let A be Interval; ::_thesis: 0 ** A is interval
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: 0 ** A is interval
hence  0 ** A is interval ; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: 0 ** A is interval
then  0 ** A = {0} by Th3;
then  0 ** A = [.0,0.] by XXREAL_1:17;
hence  0 ** A is interval ; ::_thesis: verum
end;
end;
end;

theorem Th7: :: URYSOHN2:7
for A being non empty Interval
for x being Real st x <> 0 & A is open_interval holds
x ** A is open_interval
proof
let A be non empty Interval; ::_thesis: for x being Real st x <> 0 & A is open_interval holds
x ** A is open_interval
let x be Real; ::_thesis: ( x <> 0 & A is open_interval implies x ** A is open_interval )
assume A1: x <> 0 ; ::_thesis: ( not A is open_interval or x ** A is open_interval )
assume A2: A is open_interval ; ::_thesis: x ** A is open_interval
then consider a, b being R_eal such that
A3: A = ].a,b.[ by MEASURE5:def_2;
A4: a < b by A3, XXREAL_1:28;
now__::_thesis:_(_(_x_<_0_&_x_**_A_is_open_interval_)_or_(_x_=_0_&_x_**_A_is_open_interval_)_or_(_0_<_x_&_x_**_A_is_open_interval_)_)
percases ( x < 0 or x = 0 or 0 < x ) ;
caseA5: x < 0 ; ::_thesis: x ** A is open_interval
now__::_thesis:_(_(_a_=_-infty_&_b_=_-infty_&_x_**_A_is_open_interval_)_or_(_a_=_-infty_&_b_in_REAL_&_x_**_A_is_open_interval_)_or_(_a_=_-infty_&_b_=_+infty_&_x_**_A_is_open_interval_)_or_(_a_in_REAL_&_b_in_REAL_&_x_**_A_is_open_interval_)_or_(_a_in_REAL_&_b_=_+infty_&_x_**_A_is_open_interval_)_or_(_a_=_+infty_&_b_=_+infty_&_x_**_A_is_open_interval_)_)
percases ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A4, Th5;
case ( a = -infty & b = -infty ) ; ::_thesis: x ** A is open_interval
then  ].a,b.[ = {} ;
then  x ** A = {} by A3;
hence  x ** A is open_interval ; ::_thesis: verum
end;
caseA6: ( a = -infty & b in REAL ) ; ::_thesis: x ** A is open_interval
then reconsider s = b as Real ;
set c = +infty ;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A7: d = x * s ;
A8: ].d,+infty.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].d,+infty.[ or q in x ** A )
assume A9: q in ].d,+infty.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A10: d < q1 by A9, MEASURE5:def_1;
A11: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
 x * (q / x) = q by A1, XCMPLX_1:87;
then A12: q3 < b by A5, A7, A10, XREAL_1:65;
 a < q3 by A6, XXREAL_0:12;
hence  q / x in A by A3, A12, MEASURE5:def_1; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A11, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].d,+infty.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].d,+infty.[ )
assume A13: q in x ** A ; ::_thesis: q in ].d,+infty.[
then reconsider q = q as Real ;
consider z2 being Real such that
A14: z2 in A and
A15: q = x * z2 by A13, INTEGRA2:39;
reconsider q = q as R_eal by XXREAL_0:def_1;
A16: q < +infty by XXREAL_0:9;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 z2 < b by A3, A14, MEASURE5:def_1;
then consider r, o being Real such that
A17: ( r = z2 & o = b ) and
 r <= o by A6;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def_1;
 r < o by A3, A14, A17, MEASURE5:def_1;
then  o1 < r1 by A5, XREAL_1:69;
hence  q in ].d,+infty.[ by A7, A15, A17, A16, MEASURE5:def_1; ::_thesis: verum
end;
then  x ** A = ].d,+infty.[ by A8, XBOOLE_0:def_10;
hence  x ** A is open_interval by MEASURE5:def_2; ::_thesis: verum
end;
case ( a = -infty & b = +infty ) ; ::_thesis: x ** A is open_interval
hence  x ** A is open_interval by A2, A3, A5, Th2, XXREAL_1:224; ::_thesis: verum
end;
caseA18: ( a in REAL & b in REAL ) ; ::_thesis: x ** A is open_interval
then reconsider s = a, r = b as Real ;
reconsider d = x * s, g = x * r as R_eal by XXREAL_0:def_1;
A19: ].g,d.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].g,d.[ or q in x ** A )
assume A20: q in ].g,d.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A21: q1 < d by A20, MEASURE5:def_1;
A22: g < q1 by A20, MEASURE5:def_1;
A23: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
 x * (q / x) = q by A1, XCMPLX_1:87;
then A24: a < q3 by A5, A21, XREAL_1:65;
 q / x < (x * r) / x by A5, A22, XREAL_1:75;
then  q3 < b by A5, XCMPLX_1:89;
hence  q / x in A by A3, A24, MEASURE5:def_1; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A23, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].g,d.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].g,d.[ )
assume A25: q in x ** A ; ::_thesis: q in ].g,d.[
then reconsider q = q as Real ;
consider z2 being Real such that
A26: z2 in A and
A27: q = x * z2 by A25, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a < z2 by A3, A26, MEASURE5:def_1;
then consider 1o, 1ra being Real such that
A28: ( 1o = a & 1ra = z2 ) and
 1o <= 1ra by A18;
 z2 < b by A3, A26, MEASURE5:def_1;
then consider 2o, 2r being Real such that
A29: ( 2o = z2 & 2r = b ) and
 2o <= 2r by A18;
reconsider 1o1 = x * 1o, 1r1 = x * 1ra, 2o1 = x * 2o, 2r1 = x * 2r as R_eal by XXREAL_0:def_1;
 2o < 2r by A3, A26, A29, MEASURE5:def_1;
then A30: 2r1 < 2o1 by A5, XREAL_1:69;
 1o < 1ra by A3, A26, A28, MEASURE5:def_1;
then  1r1 < 1o1 by A5, XREAL_1:69;
hence  q in ].g,d.[ by A27, A28, A29, A30, MEASURE5:def_1; ::_thesis: verum
end;
then  x ** A = ].g,d.[ by A19, XBOOLE_0:def_10;
hence  x ** A is open_interval by MEASURE5:def_2; ::_thesis: verum
end;
caseA31: ( a in REAL & b = +infty ) ; ::_thesis: x ** A is open_interval
then reconsider s = a as Real ;
set c = -infty ;
reconsider d = x * s as R_eal by XXREAL_0:def_1;
A32: ].-infty,d.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].-infty,d.[ or q in x ** A )
assume A33: q in ].-infty,d.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A34: q = x * (q / x) by A1, XCMPLX_1:87;
 q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
 q1 <= d by A33, MEASURE5:def_1;
then  x * (q / x) < x * s by A33, A34, MEASURE5:def_1;
then A35: a < q3 by A5, XREAL_1:65;
 q3 < b by A31, XXREAL_0:9;
hence  q / x in A by A3, A35, MEASURE5:def_1; ::_thesis: verum
end;
hence  q in x ** A by A34, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].-infty,d.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].-infty,d.[ )
assume A36: q in x ** A ; ::_thesis: q in ].-infty,d.[
then reconsider q = q as Real ;
consider z2 being Real such that
A37: z2 in A and
A38: q = x * z2 by A36, INTEGRA2:39;
reconsider z2 = z2, q = q as R_eal by XXREAL_0:def_1;
 a < z2 by A3, A37, MEASURE5:def_1;
then consider o, r being Real such that
A39: ( o = a & r = z2 ) and
 o <= r by A31;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def_1;
A40: -infty < q by XXREAL_0:12;
 o < r by A3, A37, A39, MEASURE5:def_1;
then  r1 < o1 by A5, XREAL_1:69;
hence  q in ].-infty,d.[ by A38, A39, A40, MEASURE5:def_1; ::_thesis: verum
end;
then  x ** A = ].-infty,d.[ by A32, XBOOLE_0:def_10;
hence  x ** A is open_interval by MEASURE5:def_2; ::_thesis: verum
end;
case ( a = +infty & b = +infty ) ; ::_thesis: x ** A is open_interval
then  ].a,b.[ = {} ;
then  x ** A = {} by A3;
hence  x ** A is open_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is open_interval ; ::_thesis: verum
end;
case x = 0 ; ::_thesis: x ** A is open_interval
hence  x ** A is open_interval by A1; ::_thesis: verum
end;
caseA41: 0 < x ; ::_thesis: x ** A is open_interval
now__::_thesis:_(_(_a_=_-infty_&_b_=_-infty_&_x_**_A_is_open_interval_)_or_(_a_=_-infty_&_b_in_REAL_&_x_**_A_is_open_interval_)_or_(_a_=_-infty_&_b_=_+infty_&_x_**_A_is_open_interval_)_or_(_a_in_REAL_&_b_in_REAL_&_x_**_A_is_open_interval_)_or_(_a_in_REAL_&_b_=_+infty_&_x_**_A_is_open_interval_)_or_(_a_=_+infty_&_b_=_+infty_&_x_**_A_is_open_interval_)_)
percases ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A4, Th5;
case ( a = -infty & b = -infty ) ; ::_thesis: x ** A is open_interval
then  ].a,b.[ = {} ;
then  x ** A = {} by A3;
hence  x ** A is open_interval ; ::_thesis: verum
end;
caseA42: ( a = -infty & b in REAL ) ; ::_thesis: x ** A is open_interval
then reconsider s = b as Real ;
set c = -infty ;
reconsider d = x * s as R_eal by XXREAL_0:def_1;
A43: ].-infty,d.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].-infty,d.[ or q in x ** A )
assume A44: q in ].-infty,d.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A45: q1 < d by A44, MEASURE5:def_1;
A46: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
 x * (q / x) = q by A1, XCMPLX_1:87;
then A47: q3 < b by A41, A45, XREAL_1:64;
 a < q3 by A42, XXREAL_0:12;
hence  q / x in A by A3, A47, MEASURE5:def_1; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A46, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].-infty,d.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].-infty,d.[ )
assume A48: q in x ** A ; ::_thesis: q in ].-infty,d.[
then reconsider q = q as Real ;
consider z2 being Real such that
A49: z2 in A and
A50: q = x * z2 by A48, INTEGRA2:39;
reconsider z2 = z2, q = q as R_eal by XXREAL_0:def_1;
 z2 < b by A3, A49, MEASURE5:def_1;
then consider r, o being Real such that
A51: ( r = z2 & o = b ) and
 r <= o by A42;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def_1;
A52: -infty < q by XXREAL_0:12;
 r < o by A3, A49, A51, MEASURE5:def_1;
then  r1 < o1 by A41, XREAL_1:68;
hence  q in ].-infty,d.[ by A50, A51, A52, MEASURE5:def_1; ::_thesis: verum
end;
then  x ** A = ].-infty,d.[ by A43, XBOOLE_0:def_10;
hence  x ** A is open_interval by MEASURE5:def_2; ::_thesis: verum
end;
case ( a = -infty & b = +infty ) ; ::_thesis: x ** A is open_interval
hence  x ** A is open_interval by A2, A3, A41, Th2, XXREAL_1:224; ::_thesis: verum
end;
caseA53: ( a in REAL & b in REAL ) ; ::_thesis: x ** A is open_interval
then reconsider s = a, r = b as Real ;
reconsider d = x * s as R_eal by XXREAL_0:def_1;
reconsider g = x * r as R_eal by XXREAL_0:def_1;
A54: ].d,g.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].d,g.[ or q in x ** A )
assume A55: q in ].d,g.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A56: q1 = q ;
A57: q1 < g by A55, A56, MEASURE5:def_1;
A58: d < q1 by A55, A56, MEASURE5:def_1;
A59: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
 x * (q / x) = q by A1, XCMPLX_1:87;
then A60: a < q3 by A41, A56, A58, XREAL_1:64;
 q / x < (x * r) / x by A41, A56, A57, XREAL_1:74;
then  q3 < b by A41, XCMPLX_1:89;
hence  q / x in A by A3, A60, MEASURE5:def_1; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A59, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].d,g.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].d,g.[ )
assume A61: q in x ** A ; ::_thesis: q in ].d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A62: z2 in A and
A63: q = x * z2 by A61, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 z2 < b by A3, A62, MEASURE5:def_1;
then consider 2o, 2r being Real such that
A64: ( 2o = z2 & 2r = b ) and
 2o <= 2r by A53;
reconsider 2o1 = x * 2o, 2r1 = x * 2r as R_eal by XXREAL_0:def_1;
 2o < 2r by A3, A62, A64, MEASURE5:def_1;
then A65: 2o1 < 2r1 by A41, XREAL_1:68;
 a < z2 by A3, A62, MEASURE5:def_1;
then consider 1o, 1ra being Real such that
A66: ( 1o = a & 1ra = z2 ) and
 1o <= 1ra by A53;
reconsider 1o1 = x * 1o, 1r1 = x * 1ra as R_eal by XXREAL_0:def_1;
 1o < 1ra by A3, A62, A66, MEASURE5:def_1;
then  1o1 < 1r1 by A41, XREAL_1:68;
hence  q in ].d,g.[ by A63, A66, A64, A65, MEASURE5:def_1; ::_thesis: verum
end;
then  x ** A = ].d,g.[ by A54, XBOOLE_0:def_10;
hence  x ** A is open_interval by MEASURE5:def_2; ::_thesis: verum
end;
caseA67: ( a in REAL & b = +infty ) ; ::_thesis: x ** A is open_interval
then reconsider s = a as Real ;
set c = +infty ;
reconsider d = x * s as R_eal by XXREAL_0:def_1;
A68: x ** A c= ].d,+infty.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].d,+infty.[ )
assume A69: q in x ** A ; ::_thesis: q in ].d,+infty.[
then reconsider q = q as Real ;
consider z2 being Real such that
A70: z2 in A and
A71: q = x * z2 by A69, INTEGRA2:39;
reconsider q = q as R_eal by XXREAL_0:def_1;
A72: q < +infty by XXREAL_0:9;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a < z2 by A3, A70, MEASURE5:def_1;
then consider o, r being Real such that
A73: ( o = a & r = z2 ) and
 o <= r by A67;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def_1;
 o < r by A3, A70, A73, MEASURE5:def_1;
then  o1 < r1 by A41, XREAL_1:68;
hence  q in ].d,+infty.[ by A71, A73, A72, MEASURE5:def_1; ::_thesis: verum
end;
 ].d,+infty.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].d,+infty.[ or q in x ** A )
assume A74: q in ].d,+infty.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A75: q = x * (q / x) by A1, XCMPLX_1:87;
A76: d < q1 by A74, MEASURE5:def_1;
 q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
 ( a < q3 & q3 < b ) by A41, A67, A76, A75, XREAL_1:64, XXREAL_0:9;
hence  q / x in A by A3, MEASURE5:def_1; ::_thesis: verum
end;
hence  q in x ** A by A75, MEMBER_1:193; ::_thesis: verum
end;
then  x ** A = ].d,+infty.[ by A68, XBOOLE_0:def_10;
hence  x ** A is open_interval by MEASURE5:def_2; ::_thesis: verum
end;
case ( a = +infty & b = +infty ) ; ::_thesis: x ** A is open_interval
then  ].a,b.[ = {} ;
then  x ** A = {} by A3;
hence  x ** A is open_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is open_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is open_interval ; ::_thesis: verum
end;

theorem Th8: :: URYSOHN2:8
for A being non empty Interval
for x being Real st x <> 0 & A is closed_interval holds
x ** A is closed_interval
proof
let A be non empty Interval; ::_thesis: for x being Real st x <> 0 & A is closed_interval holds
x ** A is closed_interval
let x be Real; ::_thesis: ( x <> 0 & A is closed_interval implies x ** A is closed_interval )
assume A1: x <> 0 ; ::_thesis: ( not A is closed_interval or x ** A is closed_interval )
assume  A is closed_interval ; ::_thesis: x ** A is closed_interval
then consider a, b being real number  such that
A2: A = [.a,b.] by MEASURE5:def_3;
reconsider a = a, b = b as R_eal by XXREAL_0:def_1;
now__::_thesis:_(_(_x_<_0_&_x_**_A_is_closed_interval_)_or_(_x_=_0_&_x_**_A_is_closed_interval_)_or_(_0_<_x_&_x_**_A_is_closed_interval_)_)
percases ( x < 0 or x = 0 or 0 < x ) ;
caseA3: x < 0 ; ::_thesis: x ** A is closed_interval
now__::_thesis:_x_**_A_is_closed_interval
reconsider s = a, r = b as Real by Th5;
reconsider d = x * s as R_eal by XXREAL_0:def_1;
reconsider g = x * r as R_eal by XXREAL_0:def_1;
A4: b in REAL by Th5;
A5: [.g,d.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.g,d.] or q in x ** A )
assume A6: q in [.g,d.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by XREAL_0:def_1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A7: g <= q1 by A6, XXREAL_1:1;
A8: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
A9: q3 <= b
proof
consider p, o being Real such that
A10: ( p = g & o = q1 ) and
A11: p <= o by A7;
 o / x <= p / x by A3, A11, XREAL_1:73;
hence  q3 <= b by A3, A10, XCMPLX_1:89; ::_thesis: verum
end;
 a <= q3
proof
 ( q1 <= d & x * (q / x) = q ) by A1, A6, XCMPLX_1:87, XXREAL_1:1;
hence  a <= q3 by A3, XREAL_1:69; ::_thesis: verum
end;
hence  q / x in A by A2, A9, XXREAL_1:1; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A8, MEMBER_1:193; ::_thesis: verum
end;
A12: a in REAL by Th5;
 x ** A c= [.g,d.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.g,d.] )
assume A13: q in x ** A ; ::_thesis: q in [.g,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A14: z2 in A and
A15: q = x * z2 by A13, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a <= z2 by A2, A14, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A16: ( 1o = a & 1ra = z2 ) and
A17: 1o <= 1ra by A12;
 z2 <= b by A2, A14, XXREAL_1:1;
then consider 2o, 2r being Real such that
A18: ( 2o = z2 & 2r = b ) and
A19: 2o <= 2r by A4;
A20: x * 2r <= x * 2o by A3, A19, XREAL_1:65;
 ( x * 1o is R_eal & x * 1ra is R_eal ) by XXREAL_0:def_1;
then consider 1o1, 1r1 being R_eal such that
A21: ( 1o1 = x * 1o & 1r1 = x * 1ra ) ;
 1r1 <= 1o1 by A3, A17, A21, XREAL_1:65;
hence  q in [.g,d.] by A15, A16, A18, A20, A21, XXREAL_1:1; ::_thesis: verum
end;
then  x ** A = [.g,d.] by A5, XBOOLE_0:def_10;
hence  x ** A is closed_interval by MEASURE5:def_3; ::_thesis: verum
end;
hence  x ** A is closed_interval ; ::_thesis: verum
end;
case x = 0 ; ::_thesis: x ** A is closed_interval
hence  x ** A is closed_interval by A1; ::_thesis: verum
end;
caseA22: 0 < x ; ::_thesis: x ** A is closed_interval
now__::_thesis:_(_a_in_REAL_&_b_in_REAL_&_x_**_A_is_closed_interval_)
percases ( a in REAL & b in REAL ) by Th5;
caseA23: ( a in REAL & b in REAL ) ; ::_thesis: x ** A is closed_interval
then reconsider r = b as Real ;
reconsider s = a as Real by A23;
reconsider g = x * r as R_eal by XXREAL_0:def_1;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A24: d = x * s ;
A25: [.d,g.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.d,g.] or q in x ** A )
assume A26: q in [.d,g.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by A24, XREAL_0:def_1;
set q2 = q / x;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A27: q1 = q ;
A28: q = x * (q / x) by A1, XCMPLX_1:87;
 q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A29: q3 = q / x ;
A30: q3 <= b
proof
 q1 <= g by A26, A27, XXREAL_1:1;
then consider p, o being Real such that
A31: ( p = q1 & o = g ) and
A32: p <= o by A27;
 p / x <= o / x by A22, A32, XREAL_1:72;
hence  q3 <= b by A22, A27, A29, A31, XCMPLX_1:89; ::_thesis: verum
end;
 a <= q3
proof
 d <= q1 by A26, A27, XXREAL_1:1;
hence  a <= q3 by A22, A24, A27, A28, A29, XREAL_1:68; ::_thesis: verum
end;
hence  q / x in A by A2, A29, A30, XXREAL_1:1; ::_thesis: verum
end;
hence  q in x ** A by A28, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= [.d,g.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.d,g.] )
assume A33: q in x ** A ; ::_thesis: q in [.d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A34: z2 in A and
A35: q = x * z2 by A33, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a <= z2 by A2, A34, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A36: ( 1o = a & 1ra = z2 ) and
A37: 1o <= 1ra by A23;
 z2 <= b by A2, A34, XXREAL_1:1;
then consider 2o, 2r being Real such that
A38: ( 2o = z2 & 2r = b ) and
A39: 2o <= 2r by A23;
A40: x * 2o <= x * 2r by A22, A39, XREAL_1:64;
 ( x * 1o is R_eal & x * 1ra is R_eal ) by XXREAL_0:def_1;
then consider 1o1, 1r1 being R_eal such that
A41: ( 1o1 = x * 1o & 1r1 = x * 1ra ) ;
 1o1 <= 1r1 by A22, A37, A41, XREAL_1:64;
hence  q in [.d,g.] by A24, A35, A36, A38, A40, A41, XXREAL_1:1; ::_thesis: verum
end;
then  x ** A = [.d,g.] by A25, XBOOLE_0:def_10;
hence  x ** A is closed_interval by A24, MEASURE5:def_3; ::_thesis: verum
end;
end;
end;
hence  x ** A is closed_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is closed_interval ; ::_thesis: verum
end;

theorem Th9: :: URYSOHN2:9
for A being non empty Interval
for x being Real st 0 < x & A is right_open_interval holds
x ** A is right_open_interval
proof
let A be non empty Interval; ::_thesis: for x being Real st 0 < x & A is right_open_interval holds
x ** A is right_open_interval
let x be Real; ::_thesis: ( 0 < x & A is right_open_interval implies x ** A is right_open_interval )
assume A1: 0 < x ; ::_thesis: ( not A is right_open_interval or x ** A is right_open_interval )
assume  A is right_open_interval ; ::_thesis: x ** A is right_open_interval
then consider a being real number , b being R_eal such that
A2: A = [.a,b.[ by MEASURE5:def_4;
A3: a < b by A2, XXREAL_1:27;
reconsider a = a as R_eal by XXREAL_0:def_1;
now__::_thesis:_(_(_a_=_-infty_&_b_=_-infty_&_x_**_A_is_right_open_interval_)_or_(_a_=_-infty_&_b_in_REAL_&_x_**_A_is_right_open_interval_)_or_(_a_=_-infty_&_b_=_+infty_&_x_**_A_is_right_open_interval_)_or_(_a_in_REAL_&_b_in_REAL_&_x_**_A_is_right_open_interval_)_or_(_a_in_REAL_&_b_=_+infty_&_x_**_A_is_right_open_interval_)_or_(_a_=_+infty_&_b_=_+infty_&_x_**_A_is_right_open_interval_)_)
percases ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A3, Th5;
case ( a = -infty & b = -infty ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
case ( a = -infty & b in REAL ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
case ( a = -infty & b = +infty ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
caseA4: ( a in REAL & b in REAL ) ; ::_thesis: x ** A is right_open_interval
then consider r being Real such that
A5: r = b ;
 x * r is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A6: g = x * r ;
consider s being Real such that
A7: s = a by A4;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A8: d = x * s ;
A9: [.d,g.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.d,g.[ or q in x ** A )
assume A10: q in [.d,g.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real by A8, XREAL_0:def_1;
set q2 = q / x;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A11: q1 = q ;
A12: q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A13: q3 = q / x ;
A14: q3 < b
proof
 q1 <= g by A10, A11, XXREAL_1:3;
then consider p, o being Real such that
A15: ( p = q1 & o = g ) and
 p <= o by A6, A11;
 p < o by A10, A11, A15, XXREAL_1:3;
then  p / x < o / x by A1, XREAL_1:74;
hence  q3 < b by A1, A5, A6, A11, A13, A15, XCMPLX_1:89; ::_thesis: verum
end;
 a <= q3
proof
 ( d <= q1 & x * (q / x) = q ) by A1, A10, A11, XCMPLX_1:87, XXREAL_1:3;
hence  a <= q3 by A1, A7, A8, A11, A13, XREAL_1:68; ::_thesis: verum
end;
hence  q / x in A by A2, A13, A14, XXREAL_1:3; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A12, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= [.d,g.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.d,g.[ )
assume A16: q in x ** A ; ::_thesis: q in [.d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A17: z2 in A and
A18: q = x * z2 by A16, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 z2 <= b by A2, A17, XXREAL_1:3;
then consider 2o, 2r being Real such that
A19: ( 2o = z2 & 2r = b ) and
 2o <= 2r by A4;
 ( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def_1;
then consider 2o1, 2r1 being R_eal such that
A20: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
 2o < 2r by A2, A17, A19, XXREAL_1:3;
then A21: 2o1 < 2r1 by A1, A20, XREAL_1:68;
 a <= z2 by A2, A17, XXREAL_1:3;
then consider 1o, 1ra being Real such that
A22: ( 1o = a & 1ra = z2 ) and
A23: 1o <= 1ra by A4;
 x * 1o <= x * 1ra by A1, A23, XREAL_1:64;
hence  q in [.d,g.[ by A7, A5, A8, A6, A18, A22, A19, A20, A21, XXREAL_1:3; ::_thesis: verum
end;
then  x ** A = [.d,g.[ by A9, XBOOLE_0:def_10;
hence  x ** A is right_open_interval by A8, MEASURE5:def_4; ::_thesis: verum
end;
caseA24: ( a in REAL & b = +infty ) ; ::_thesis: x ** A is right_open_interval
then consider s being Real such that
A25: s = a ;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A26: d = x * s ;
consider c being R_eal such that
A27: c = +infty ;
A28: [.d,c.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.d,c.[ or q in x ** A )
assume A29: q in [.d,c.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real by A26, XREAL_0:def_1;
set q2 = q / x;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A30: q1 = q ;
A31: q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A32: q3 = q / x ;
A33: a <= q3
proof
 ( d <= q1 & x * (q / x) = q ) by A1, A29, A30, XCMPLX_1:87, XXREAL_1:3;
hence  a <= q3 by A1, A25, A26, A30, A32, XREAL_1:68; ::_thesis: verum
end;
 q3 < b by A24, A32, XXREAL_0:9;
hence  q / x in A by A2, A32, A33, XXREAL_1:3; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A31, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= [.d,c.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.d,c.[ )
assume A34: q in x ** A ; ::_thesis: q in [.d,c.[
then reconsider q = q as Real ;
consider z2 being Real such that
A35: z2 in A and
A36: q = x * z2 by A34, INTEGRA2:39;
reconsider q = q as R_eal by XXREAL_0:def_1;
A37: q < +infty by XXREAL_0:9;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a <= z2 by A2, A35, XXREAL_1:3;
then consider o, r being Real such that
A38: ( o = a & r = z2 ) and
A39: o <= r by A24;
 x * o <= x * r by A1, A39, XREAL_1:64;
hence  q in [.d,c.[ by A25, A27, A26, A36, A38, A37, XXREAL_1:3; ::_thesis: verum
end;
then  x ** A = [.d,c.[ by A28, XBOOLE_0:def_10;
hence  x ** A is right_open_interval by A26, MEASURE5:def_4; ::_thesis: verum
end;
case ( a = +infty & b = +infty ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is right_open_interval ; ::_thesis: verum
end;

theorem Th10: :: URYSOHN2:10
for A being non empty Interval
for x being Real st x < 0 & A is right_open_interval holds
x ** A is left_open_interval
proof
let A be non empty Interval; ::_thesis: for x being Real st x < 0 & A is right_open_interval holds
x ** A is left_open_interval
let x be Real; ::_thesis: ( x < 0 & A is right_open_interval implies x ** A is left_open_interval )
assume A1: x < 0 ; ::_thesis: ( not A is right_open_interval or x ** A is left_open_interval )
assume  A is right_open_interval ; ::_thesis: x ** A is left_open_interval
then consider a being real number , b being R_eal such that
A2: A = [.a,b.[ by MEASURE5:def_4;
A3: a < b by A2, XXREAL_1:27;
reconsider a = a as R_eal by XXREAL_0:def_1;
now__::_thesis:_(_(_a_=_-infty_&_b_=_-infty_&_x_**_A_is_left_open_interval_)_or_(_a_=_-infty_&_b_in_REAL_&_x_**_A_is_left_open_interval_)_or_(_a_=_-infty_&_b_=_+infty_&_x_**_A_is_left_open_interval_)_or_(_a_in_REAL_&_b_in_REAL_&_x_**_A_is_left_open_interval_)_or_(_a_in_REAL_&_b_=_+infty_&_x_**_A_is_left_open_interval_)_or_(_a_=_+infty_&_b_=_+infty_&_x_**_A_is_left_open_interval_)_)
percases ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A3, Th5;
case ( a = -infty & b = -infty ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
case ( a = -infty & b in REAL ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
case ( a = -infty & b = +infty ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
caseA4: ( a in REAL & b in REAL ) ; ::_thesis: x ** A is left_open_interval
then consider r being Real such that
A5: r = b ;
 x * r is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A6: g = x * r ;
consider s being Real such that
A7: s = a by A4;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A8: d = x * s ;
A9: ].g,d.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].g,d.] or q in x ** A )
assume A10: q in ].g,d.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by A8, XREAL_0:def_1;
set q2 = q / x;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A11: q1 = q ;
A12: g < q1 by A10, A11, XXREAL_1:2;
A13: q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A14: q3 = q / x ;
A15: q3 < b
proof
consider p, o being Real such that
A16: ( p = g & o = q1 ) and
 p <= o by A6, A11, A12;
 g < q1 by A10, A11, XXREAL_1:2;
then  o / x < p / x by A1, A16, XREAL_1:75;
hence  q3 < b by A1, A5, A6, A11, A14, A16, XCMPLX_1:89; ::_thesis: verum
end;
 a <= q3
proof
 ( q1 <= d & x * (q / x) = q ) by A1, A10, A11, XCMPLX_1:87, XXREAL_1:2;
hence  a <= q3 by A1, A7, A8, A11, A14, XREAL_1:69; ::_thesis: verum
end;
hence  q / x in A by A2, A14, A15, XXREAL_1:3; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A13, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].g,d.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].g,d.] )
assume A17: q in x ** A ; ::_thesis: q in ].g,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 z2 <= b by A2, A18, XXREAL_1:3;
then consider 2o, 2r being Real such that
A20: ( 2o = z2 & 2r = b ) and
 2o <= 2r by A4;
 ( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def_1;
then consider 2o1, 2r1 being R_eal such that
A21: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
 2o < 2r by A2, A18, A20, XXREAL_1:3;
then A22: 2r1 < 2o1 by A1, A21, XREAL_1:69;
 a <= z2 by A2, A18, XXREAL_1:3;
then consider 1o, 1ra being Real such that
A23: ( 1o = a & 1ra = z2 ) and
A24: 1o <= 1ra by A4;
 x * 1ra <= x * 1o by A1, A24, XREAL_1:65;
hence  q in ].g,d.] by A7, A5, A8, A6, A19, A23, A20, A21, A22, XXREAL_1:2; ::_thesis: verum
end;
then  x ** A = ].g,d.] by A9, XBOOLE_0:def_10;
hence  x ** A is left_open_interval by A8, MEASURE5:def_5; ::_thesis: verum
end;
caseA25: ( a in REAL & b = +infty ) ; ::_thesis: x ** A is left_open_interval
then consider s being Real such that
A26: s = a ;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A27: d = x * s ;
consider c being R_eal such that
A28: c = -infty ;
A29: ].c,d.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].c,d.] or q in x ** A )
assume A30: q in ].c,d.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by A27, XREAL_0:def_1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A31: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
A32: a <= q3
proof
 ( q1 <= d & x * (q / x) = q ) by A1, A30, XCMPLX_1:87, XXREAL_1:2;
hence  a <= q3 by A1, A26, A27, XREAL_1:69; ::_thesis: verum
end;
 q3 < b by A25, XXREAL_0:9;
hence  q / x in A by A2, A32, XXREAL_1:3; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A31, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].c,d.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].c,d.] )
assume A33: q in x ** A ; ::_thesis: q in ].c,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A34: z2 in A and
A35: q = x * z2 by A33, INTEGRA2:39;
reconsider q = q as R_eal by XXREAL_0:def_1;
A36: -infty < q by XXREAL_0:12;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a <= z2 by A2, A34, XXREAL_1:3;
then consider o, r being Real such that
A37: ( o = a & r = z2 ) and
A38: o <= r by A25;
 x * r <= x * o by A1, A38, XREAL_1:65;
hence  q in ].c,d.] by A26, A28, A27, A35, A37, A36, XXREAL_1:2; ::_thesis: verum
end;
then  x ** A = ].c,d.] by A29, XBOOLE_0:def_10;
hence  x ** A is left_open_interval by A27, MEASURE5:def_5; ::_thesis: verum
end;
case ( a = +infty & b = +infty ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is left_open_interval ; ::_thesis: verum
end;

theorem Th11: :: URYSOHN2:11
for A being non empty Interval
for x being Real st 0 < x & A is left_open_interval holds
x ** A is left_open_interval
proof
let A be non empty Interval; ::_thesis: for x being Real st 0 < x & A is left_open_interval holds
x ** A is left_open_interval
let x be Real; ::_thesis: ( 0 < x & A is left_open_interval implies x ** A is left_open_interval )
assume A1: 0 < x ; ::_thesis: ( not A is left_open_interval or x ** A is left_open_interval )
assume  A is left_open_interval ; ::_thesis: x ** A is left_open_interval
then consider a being R_eal, b being real number  such that
A2: A = ].a,b.] by MEASURE5:def_5;
A3: a < b by A2, XXREAL_1:26;
reconsider b = b as R_eal by XXREAL_0:def_1;
now__::_thesis:_(_(_a_=_-infty_&_b_=_-infty_&_x_**_A_is_left_open_interval_)_or_(_a_=_-infty_&_b_in_REAL_&_x_**_A_is_left_open_interval_)_or_(_a_=_-infty_&_b_=_+infty_&_x_**_A_is_left_open_interval_)_or_(_a_in_REAL_&_b_in_REAL_&_x_**_A_is_left_open_interval_)_or_(_a_in_REAL_&_b_=_+infty_&_x_**_A_is_left_open_interval_)_or_(_a_=_+infty_&_b_=_+infty_&_x_**_A_is_left_open_interval_)_)
percases ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A3, Th5;
case ( a = -infty & b = -infty ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
caseA4: ( a = -infty & b in REAL ) ; ::_thesis: x ** A is left_open_interval
then consider s being Real such that
A5: s = b ;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A6: d = x * s ;
consider c being R_eal such that
A7: c = -infty ;
A8: ].c,d.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].c,d.] or q in x ** A )
assume A9: q in ].c,d.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by A6, XREAL_0:def_1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A10: q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A11: q3 = q / x ;
A12: q3 <= b
proof
 ( q1 <= d & x * (q / x) = q ) by A1, A9, XCMPLX_1:87, XXREAL_1:2;
hence  q3 <= b by A1, A5, A6, A11, XREAL_1:68; ::_thesis: verum
end;
 a < q3 by A4, A11, XXREAL_0:12;
hence  q / x in A by A2, A11, A12, XXREAL_1:2; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A10, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].c,d.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].c,d.] )
assume A13: q in x ** A ; ::_thesis: q in ].c,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A14: z2 in A and
A15: q = x * z2 by A13, INTEGRA2:39;
reconsider q = q as R_eal by XXREAL_0:def_1;
A16: -infty < q by XXREAL_0:12;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 z2 <= b by A2, A14, XXREAL_1:2;
then consider r, o being Real such that
A17: ( r = z2 & o = b ) and
A18: r <= o by A4;
 x * r <= x * o by A1, A18, XREAL_1:64;
hence  q in ].c,d.] by A5, A7, A6, A15, A17, A16, XXREAL_1:2; ::_thesis: verum
end;
then  x ** A = ].c,d.] by A8, XBOOLE_0:def_10;
hence  x ** A is left_open_interval by A6, MEASURE5:def_5; ::_thesis: verum
end;
case ( a = -infty & b = +infty ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
caseA19: ( a in REAL & b in REAL ) ; ::_thesis: x ** A is left_open_interval
then reconsider s = a as Real ;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A20: d = x * s ;
consider r being Real such that
A21: r = b by A19;
 x * r is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A22: g = x * r ;
A23: ].d,g.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].d,g.] or q in x ** A )
assume A24: q in ].d,g.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by A22, XREAL_0:def_1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A25: q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A26: q3 = q / x ;
A27: q3 <= b
proof
 q1 <= g by A24, XXREAL_1:2;
then consider p, o being Real such that
A28: ( p = q1 & o = g ) and
A29: p <= o by A22;
 p / x <= o / x by A1, A29, XREAL_1:72;
hence  q3 <= b by A1, A21, A22, A26, A28, XCMPLX_1:89; ::_thesis: verum
end;
 ( d < q1 & x * (q / x) = q ) by A1, A24, XCMPLX_1:87, XXREAL_1:2;
then  a < q3 by A1, A20, A26, XREAL_1:64;
hence  q / x in A by A2, A26, A27, XXREAL_1:2; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A25, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].d,g.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].d,g.] )
assume A30: q in x ** A ; ::_thesis: q in ].d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A31: z2 in A and
A32: q = x * z2 by A30, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a <= z2 by A2, A31, XXREAL_1:2;
then consider 1o, 1ra being Real such that
A33: ( 1o = a & 1ra = z2 ) and
 1o <= 1ra by A19;
 1o < 1ra by A2, A31, A33, XXREAL_1:2;
then A34: x * 1o < x * 1ra by A1, XREAL_1:68;
 z2 <= b by A2, A31, XXREAL_1:2;
then consider 2o, 2r being Real such that
A35: ( 2o = z2 & 2r = b ) and
A36: 2o <= 2r by A19;
 ( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def_1;
then consider 2o1, 2r1 being R_eal such that
A37: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
 2o1 <= 2r1 by A1, A36, A37, XREAL_1:64;
hence  q in ].d,g.] by A21, A20, A22, A32, A33, A35, A34, A37, XXREAL_1:2; ::_thesis: verum
end;
then  x ** A = ].d,g.] by A23, XBOOLE_0:def_10;
hence  x ** A is left_open_interval by A22, MEASURE5:def_5; ::_thesis: verum
end;
case ( a in REAL & b = +infty ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
case ( a = +infty & b = +infty ) ; ::_thesis: x ** A is left_open_interval
hence  x ** A is left_open_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is left_open_interval ; ::_thesis: verum
end;

theorem Th12: :: URYSOHN2:12
for A being non empty Interval
for x being Real st x < 0 & A is left_open_interval holds
x ** A is right_open_interval
proof
let A be non empty Interval; ::_thesis: for x being Real st x < 0 & A is left_open_interval holds
x ** A is right_open_interval
let x be Real; ::_thesis: ( x < 0 & A is left_open_interval implies x ** A is right_open_interval )
assume A1: x < 0 ; ::_thesis: ( not A is left_open_interval or x ** A is right_open_interval )
assume  A is left_open_interval ; ::_thesis: x ** A is right_open_interval
then consider a being R_eal, b being real number  such that
A2: A = ].a,b.] by MEASURE5:def_5;
A3: a < b by A2, XXREAL_1:26;
reconsider b = b as R_eal by XXREAL_0:def_1;
now__::_thesis:_(_(_a_=_-infty_&_b_=_-infty_&_x_**_A_is_right_open_interval_)_or_(_a_=_-infty_&_b_in_REAL_&_x_**_A_is_right_open_interval_)_or_(_a_=_-infty_&_b_=_+infty_&_x_**_A_is_right_open_interval_)_or_(_a_in_REAL_&_b_in_REAL_&_x_**_A_is_right_open_interval_)_or_(_a_in_REAL_&_b_=_+infty_&_x_**_A_is_right_open_interval_)_or_(_a_=_+infty_&_b_=_+infty_&_x_**_A_is_right_open_interval_)_)
percases ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A3, Th5;
case ( a = -infty & b = -infty ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
caseA4: ( a = -infty & b in REAL ) ; ::_thesis: x ** A is right_open_interval
then consider s being Real such that
A5: s = b ;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A6: d = x * s ;
consider c being R_eal such that
A7: c = +infty ;
A8: [.d,c.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.d,c.[ or q in x ** A )
assume A9: q in [.d,c.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real by A6, XREAL_0:def_1;
consider q2 being Real such that
A10: q2 = q / x ;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A11: q1 = q ;
A12: q2 in A
proof
 q2 is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A13: q3 = q2 ;
A14: q3 <= b
proof
 ( d <= q1 & x * q2 = q ) by A1, A9, A11, A10, XCMPLX_1:87, XXREAL_1:3;
hence  q3 <= b by A1, A5, A6, A11, A13, XREAL_1:69; ::_thesis: verum
end;
 a < q3 by A4, A13, XXREAL_0:12;
hence  q2 in A by A2, A13, A14, XXREAL_1:2; ::_thesis: verum
end;
 q = x * q2 by A1, A10, XCMPLX_1:87;
hence  q in x ** A by A12, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= [.d,c.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.d,c.[ )
assume A15: q in x ** A ; ::_thesis: q in [.d,c.[
then reconsider q = q as Real ;
consider z2 being Real such that
A16: z2 in A and
A17: q = x * z2 by A15, INTEGRA2:39;
reconsider q = q as R_eal by XXREAL_0:def_1;
A18: q < +infty by XXREAL_0:9;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 z2 <= b by A2, A16, XXREAL_1:2;
then consider r, o being Real such that
A19: ( r = z2 & o = b ) and
A20: r <= o by A4;
 x * o <= x * r by A1, A20, XREAL_1:65;
hence  q in [.d,c.[ by A5, A7, A6, A17, A19, A18, XXREAL_1:3; ::_thesis: verum
end;
then  x ** A = [.d,c.[ by A8, XBOOLE_0:def_10;
hence  x ** A is right_open_interval by A6, MEASURE5:def_4; ::_thesis: verum
end;
case ( a = -infty & b = +infty ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
caseA21: ( a in REAL & b in REAL ) ; ::_thesis: x ** A is right_open_interval
then reconsider s = a, r = b as Real ;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A22: d = x * s ;
 x * r is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A23: g = x * r ;
A24: [.g,d.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.g,d.[ or q in x ** A )
assume A25: q in [.g,d.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real by A23, XREAL_0:def_1;
consider q2 being Real such that
A26: q2 = q / x ;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A27: q1 = q ;
A28: q1 < d by A25, A27, XXREAL_1:3;
A29: q2 in A
proof
 q2 is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A30: q3 = q2 ;
A31: q3 <= b
proof
 g <= q1 by A25, A27, XXREAL_1:3;
then consider p, o being Real such that
A32: ( p = g & o = q1 ) and
A33: p <= o by A23, A27;
 o / x <= p / x by A1, A33, XREAL_1:73;
hence  q3 <= b by A1, A23, A27, A26, A30, A32, XCMPLX_1:89; ::_thesis: verum
end;
 x * q2 = q by A1, A26, XCMPLX_1:87;
then  a < q3 by A1, A22, A27, A28, A30, XREAL_1:65;
hence  q2 in A by A2, A30, A31, XXREAL_1:2; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A26, A29, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= [.g,d.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.g,d.[ )
assume A34: q in x ** A ; ::_thesis: q in [.g,d.[
then reconsider q = q as Real ;
consider z2 being Real such that
A35: z2 in A and
A36: q = x * z2 by A34, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 a <= z2 by A2, A35, XXREAL_1:2;
then consider 1o, 1ra being Real such that
A37: ( 1o = a & 1ra = z2 ) and
 1o <= 1ra by A21;
 1o < 1ra by A2, A35, A37, XXREAL_1:2;
then A38: x * 1ra < x * 1o by A1, XREAL_1:69;
 z2 <= b by A2, A35, XXREAL_1:2;
then consider 2o, 2r being Real such that
A39: ( 2o = z2 & 2r = b ) and
A40: 2o <= 2r by A21;
 ( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def_1;
then consider 2o1, 2r1 being R_eal such that
A41: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
 2r1 <= 2o1 by A1, A40, A41, XREAL_1:65;
hence  q in [.g,d.[ by A22, A23, A36, A37, A39, A38, A41, XXREAL_1:3; ::_thesis: verum
end;
then  x ** A = [.g,d.[ by A24, XBOOLE_0:def_10;
hence  x ** A is right_open_interval by A23, MEASURE5:def_4; ::_thesis: verum
end;
case ( a in REAL & b = +infty ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
case ( a = +infty & b = +infty ) ; ::_thesis: x ** A is right_open_interval
hence  x ** A is right_open_interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is right_open_interval ; ::_thesis: verum
end;

theorem :: URYSOHN2:13
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).] holds
( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
proof
let A be non empty Interval; ::_thesis: for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).] holds
( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let x be Real; ::_thesis: ( 0 < x implies for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).] holds
( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A1: 0 < x ; ::_thesis: for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).] holds
( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let B be non empty Interval; ::_thesis: ( B = x ** A & A = [.(inf A),(sup A).] implies ( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A2: B = x ** A ; ::_thesis: ( not A = [.(inf A),(sup A).] or ( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
 ( A = [.(inf A),(sup A).] implies ( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
proof
assume A3: A = [.(inf A),(sup A).] ; ::_thesis: ( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
A4: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t )
proof
let s, t be Real; ::_thesis: ( s = inf A & t = sup A implies ( inf B = x * s & sup B = x * t ) )
assume that
A5: s = inf A and
A6: t = sup A ; ::_thesis: ( inf B = x * s & sup B = x * t )
 ( inf B = x * s & sup B = x * t )
proof
 s <= t by A5, A6, XXREAL_2:40;
then A7: x * s <= x * t by A1, XREAL_1:64;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A8: d = x * s ;
 x * t is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A9: g = x * t ;
A10: [.d,g.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.d,g.] or q in x ** A )
assume A11: q in [.d,g.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by A8, A9, XREAL_0:def_1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A12: q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A13: q3 = q / x ;
A14: q3 <= sup A
proof
 q1 <= g by A11, XXREAL_1:1;
then consider p, o being Real such that
A15: ( p = q1 & o = g ) and
A16: p <= o by A9;
 p / x <= o / x by A1, A16, XREAL_1:72;
hence  q3 <= sup A by A1, A6, A9, A13, A15, XCMPLX_1:89; ::_thesis: verum
end;
 inf A <= q3
proof
 ( d <= q1 & x * (q / x) = q ) by A1, A11, XCMPLX_1:87, XXREAL_1:1;
hence  inf A <= q3 by A1, A5, A8, A13, XREAL_1:68; ::_thesis: verum
end;
hence  q / x in A by A3, A13, A14, XXREAL_1:1; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A12, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= [.d,g.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.d,g.] )
assume A17: q in x ** A ; ::_thesis: q in [.d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 inf A <= z2 by A3, A18, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A20: ( 1o = inf A & 1ra = z2 ) and
A21: 1o <= 1ra by A5;
A22: x * 1o <= x * 1ra by A1, A21, XREAL_1:64;
 z2 <= sup A by A3, A18, XXREAL_1:1;
then consider 2o, 2r being Real such that
A23: ( 2o = z2 & 2r = sup A ) and
A24: 2o <= 2r by A6;
 ( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def_1;
then consider 2o1, 2r1 being R_eal such that
A25: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
 2o1 <= 2r1 by A1, A24, A25, XREAL_1:64;
hence  q in [.d,g.] by A5, A6, A8, A9, A19, A20, A23, A22, A25, XXREAL_1:1; ::_thesis: verum
end;
then  x ** A = [.d,g.] by A10, XBOOLE_0:def_10;
hence  ( inf B = x * s & sup B = x * t ) by A2, A8, A9, A7, MEASURE6:10, MEASURE6:14; ::_thesis: verum
end;
hence  ( inf B = x * s & sup B = x * t ) ; ::_thesis: verum
end;
 inf A <= sup A by XXREAL_2:40;
then  ( inf A in A & sup A in A ) by A3, XXREAL_1:1;
then  A is closed_interval by A3, MEASURE5:def_3;
then  x ** A is closed_interval by A1, Th8;
hence  ( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) by A2, A4, MEASURE6:17; ::_thesis: verum
end;
hence  ( not A = [.(inf A),(sup A).] or ( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) ) ; ::_thesis: verum
end;

theorem :: URYSOHN2:14
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).] holds
( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
proof
let A be non empty Interval; ::_thesis: for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).] holds
( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let x be Real; ::_thesis: ( 0 < x implies for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).] holds
( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A1: 0 < x ; ::_thesis: for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).] holds
( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let B be non empty Interval; ::_thesis: ( B = x ** A & A = ].(inf A),(sup A).] implies ( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A2: B = x ** A ; ::_thesis: ( not A = ].(inf A),(sup A).] or ( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
A3: inf A <= sup A by XXREAL_2:40;
assume A4: A = ].(inf A),(sup A).] ; ::_thesis: ( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
then  inf A <> sup A ;
then  inf A < sup A by A3, XXREAL_0:1;
then  sup A in A by A4, XXREAL_1:2;
then reconsider b = sup A as real number ;
A5: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t )
proof
let s, t be Real; ::_thesis: ( s = inf A & t = sup A implies ( inf B = x * s & sup B = x * t ) )
assume that
A6: s = inf A and
A7: t = sup A ; ::_thesis: ( inf B = x * s & sup B = x * t )
 ( inf B = x * s & sup B = x * t )
proof
 s <= t by A6, A7, XXREAL_2:40;
then A8: x * s <= x * t by A1, XREAL_1:64;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A9: d = x * s ;
 x * t is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A10: g = x * t ;
A11: ].d,g.] c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].d,g.] or q in x ** A )
assume A12: q in ].d,g.] ; ::_thesis: q in x ** A
then reconsider q = q as Real by A10, XREAL_0:def_1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A13: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
A14: q3 <= sup A
proof
 q1 <= g by A12, XXREAL_1:2;
then consider p, o being Real such that
A15: ( p = q1 & o = g ) and
A16: p <= o by A10;
 p / x <= o / x by A1, A16, XREAL_1:72;
hence  q3 <= sup A by A1, A7, A10, A15, XCMPLX_1:89; ::_thesis: verum
end;
 ( d < q1 & x * (q / x) = q ) by A1, A12, XCMPLX_1:87, XXREAL_1:2;
then  inf A < q3 by A1, A6, A9, XREAL_1:64;
hence  q / x in A by A4, A14, XXREAL_1:2; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A13, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].d,g.]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].d,g.] )
assume A17: q in x ** A ; ::_thesis: q in ].d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
reconsider q = q as R_eal by XXREAL_0:def_1;
 inf A <= z2 by A4, A18, XXREAL_1:2;
then consider 1o, 1ra being Real such that
A20: ( 1o = inf A & 1ra = z2 ) and
 1o <= 1ra by A6;
 1o < 1ra by A4, A18, A20, XXREAL_1:2;
then A21: d < q by A1, A6, A9, A19, A20, XREAL_1:68;
 z2 <= sup A by A4, A18, XXREAL_1:2;
then consider 2o, 2r being Real such that
A22: ( 2o = z2 & 2r = sup A ) and
A23: 2o <= 2r by A7;
 x * 2o <= x * 2r by A1, A23, XREAL_1:64;
hence  q in ].d,g.] by A7, A10, A19, A22, A21, XXREAL_1:2; ::_thesis: verum
end;
then  x ** A = ].d,g.] by A11, XBOOLE_0:def_10;
hence  ( inf B = x * s & sup B = x * t ) by A2, A9, A10, A8, MEASURE6:9, MEASURE6:13; ::_thesis: verum
end;
hence  ( inf B = x * s & sup B = x * t ) ; ::_thesis: verum
end;
 A = ].(inf A),b.] by A4;
then  A is left_open_interval by MEASURE5:def_5;
then  B is left_open_interval by A1, A2, Th11;
hence  ( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) by A5, MEASURE6:19; ::_thesis: verum
end;

theorem :: URYSOHN2:15
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
proof
let A be non empty Interval; ::_thesis: for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let x be Real; ::_thesis: ( 0 < x implies for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A1: 0 < x ; ::_thesis: for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds
( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let B be non empty Interval; ::_thesis: ( B = x ** A & A = ].(inf A),(sup A).[ implies ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A2: B = x ** A ; ::_thesis: ( not A = ].(inf A),(sup A).[ or ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
 ( A = ].(inf A),(sup A).[ implies ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
proof
assume A3: A = ].(inf A),(sup A).[ ; ::_thesis: ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
A4: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t & B is open_interval )
proof
let s, t be Real; ::_thesis: ( s = inf A & t = sup A implies ( inf B = x * s & sup B = x * t & B is open_interval ) )
assume that
A5: s = inf A and
A6: t = sup A ; ::_thesis: ( inf B = x * s & sup B = x * t & B is open_interval )
 ( inf B = x * s & sup B = x * t & B is open_interval )
proof
 s <= t by A5, A6, XXREAL_2:40;
then A7: x * s <= x * t by A1, XREAL_1:64;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A8: d = x * s ;
 x * t is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A9: g = x * t ;
A10: ].d,g.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ].d,g.[ or q in x ** A )
assume A11: q in ].d,g.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real ;
set q2 = q / x;
 q is R_eal by XXREAL_0:def_1;
then consider q1 being R_eal such that
A12: q1 = q ;
A13: q1 < g by A11, A12, MEASURE5:def_1;
A14: q / x in A
proof
 q / x is R_eal by XXREAL_0:def_1;
then consider q3 being R_eal such that
A15: q3 = q / x ;
A16: q3 < sup A
proof
consider p, o being Real such that
A17: ( p = q1 & o = g ) and
 p <= o by A9, A12, A13;
 p / x < o / x by A1, A13, A17, XREAL_1:74;
hence  q3 < sup A by A1, A6, A9, A12, A15, A17, XCMPLX_1:89; ::_thesis: verum
end;
 ( d < q1 & x * (q / x) = q ) by A1, A11, A12, MEASURE5:def_1, XCMPLX_1:87;
then  inf A < q3 by A1, A5, A8, A12, A15, XREAL_1:64;
hence  q / x in A by A3, A15, A16, MEASURE5:def_1; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A14, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= ].d,g.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in ].d,g.[ )
assume A18: q in x ** A ; ::_thesis: q in ].d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A19: z2 in A and
A20: q = x * z2 by A18, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 inf A <= z2 by A3, A19, MEASURE5:def_1;
then consider 1o, 1ra being Real such that
A21: ( 1o = inf A & 1ra = z2 ) and
 1o <= 1ra by A5;
 1o < 1ra by A3, A19, A21, MEASURE5:def_1;
then A22: x * 1o < x * 1ra by A1, XREAL_1:68;
 z2 <= sup A by A3, A19, MEASURE5:def_1;
then consider 2o, 2r being Real such that
A23: ( 2o = z2 & 2r = sup A ) and
 2o <= 2r by A6;
 ( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def_1;
then consider 2o1, 2r1 being R_eal such that
A24: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
 2o < 2r by A3, A19, A23, MEASURE5:def_1;
then  2o1 < 2r1 by A1, A24, XREAL_1:68;
hence  q in ].d,g.[ by A5, A6, A8, A9, A20, A21, A23, A22, A24, MEASURE5:def_1; ::_thesis: verum
end;
then  x ** A = ].d,g.[ by A10, XBOOLE_0:def_10;
hence  ( inf B = x * s & sup B = x * t & B is open_interval ) by A2, A8, A9, A7, MEASURE5:def_2, MEASURE6:8, MEASURE6:12; ::_thesis: verum
end;
hence  ( inf B = x * s & sup B = x * t & B is open_interval ) ; ::_thesis: verum
end;
 A is open_interval by A3, MEASURE5:def_2;
then  x ** A is open_interval by A1, Th7;
hence  ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) by A2, A4, MEASURE6:16; ::_thesis: verum
end;
hence  ( not A = ].(inf A),(sup A).[ or ( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) ) ; ::_thesis: verum
end;

theorem :: URYSOHN2:16
for A being non empty Interval
for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
proof
let A be non empty Interval; ::_thesis: for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let x be Real; ::_thesis: ( 0 < x implies for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A1: 0 < x ; ::_thesis: for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let B be non empty Interval; ::_thesis: ( B = x ** A & A = [.(inf A),(sup A).[ implies ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A2: B = x ** A ; ::_thesis: ( not A = [.(inf A),(sup A).[ or ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
A3: inf A <= sup A by XXREAL_2:40;
assume A4: A = [.(inf A),(sup A).[ ; ::_thesis: ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
then  inf A <> sup A ;
then  inf A < sup A by A3, XXREAL_0:1;
then  inf A in A by A4, XXREAL_1:3;
then reconsider a = inf A as real number ;
A5: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t & B is right_open_interval )
proof
let s, t be Real; ::_thesis: ( s = inf A & t = sup A implies ( inf B = x * s & sup B = x * t & B is right_open_interval ) )
assume that
A6: s = inf A and
A7: t = sup A ; ::_thesis: ( inf B = x * s & sup B = x * t & B is right_open_interval )
 ( inf B = x * s & sup B = x * t & B is right_open_interval )
proof
 s <= t by A6, A7, XXREAL_2:40;
then A8: x * s <= x * t by A1, XREAL_1:64;
 x * s is R_eal by XXREAL_0:def_1;
then consider d being R_eal such that
A9: d = x * s ;
 x * t is R_eal by XXREAL_0:def_1;
then consider g being R_eal such that
A10: g = x * t ;
A11: [.d,g.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [.d,g.[ or q in x ** A )
assume A12: q in [.d,g.[ ; ::_thesis: q in x ** A
then reconsider q = q as Real by A9, XREAL_0:def_1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def_1;
A13: q1 < g by A12, XXREAL_1:3;
A14: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def_1;
 ( inf A <= q3 & q3 < sup A & q3 in REAL )
proof
A15: q3 < sup A
proof
consider p, o being Real such that
A16: ( p = q1 & o = g ) and
 p <= o by A10, A13;
 q1 < g by A12, XXREAL_1:3;
then  p / x < o / x by A1, A16, XREAL_1:74;
hence  q3 < sup A by A1, A7, A10, A16, XCMPLX_1:89; ::_thesis: verum
end;
 ( d <= q1 & x * (q / x) = q ) by A1, A12, XCMPLX_1:87, XXREAL_1:3;
hence  ( inf A <= q3 & q3 < sup A & q3 in REAL ) by A1, A6, A9, A15, XREAL_1:68; ::_thesis: verum
end;
hence  q / x in A by A4, XXREAL_1:3; ::_thesis: verum
end;
 q = x * (q / x) by A1, XCMPLX_1:87;
hence  q in x ** A by A14, MEMBER_1:193; ::_thesis: verum
end;
 x ** A c= [.d,g.[
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in x ** A or q in [.d,g.[ )
assume A17: q in x ** A ; ::_thesis: q in [.d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def_1;
 z2 <= sup A by A4, A18, XXREAL_1:3;
then consider 2o, 2r being Real such that
A20: ( 2o = z2 & 2r = sup A ) and
 2o <= 2r by A7;
 ( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def_1;
then consider 2o1, 2r1 being R_eal such that
A21: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
 2o < 2r by A4, A18, A20, XXREAL_1:3;
then A22: 2o1 < 2r1 by A1, A21, XREAL_1:68;
 inf A <= z2 by A4, A18, XXREAL_1:3;
then consider 1o, 1ra being Real such that
A23: ( 1o = inf A & 1ra = z2 ) and
A24: 1o <= 1ra by A6;
 x * 1o <= x * 1ra by A1, A24, XREAL_1:64;
hence  q in [.d,g.[ by A6, A7, A9, A10, A19, A23, A20, A21, A22, XXREAL_1:3; ::_thesis: verum
end;
then  x ** A = [.d,g.[ by A11, XBOOLE_0:def_10;
hence  ( inf B = x * s & sup B = x * t & B is right_open_interval ) by A2, A9, A10, A8, MEASURE5:def_4, MEASURE6:11, MEASURE6:15; ::_thesis: verum
end;
hence  ( inf B = x * s & sup B = x * t & B is right_open_interval ) ; ::_thesis: verum
end;
 A = [.a,(sup A).[ by A4;
then  A is right_open_interval by MEASURE5:def_4;
then  x ** A is right_open_interval by A1, Th9;
hence  ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) by A2, A5, MEASURE6:18; ::_thesis: verum
end;

theorem Th17: :: URYSOHN2:17
for A being non empty Interval
for x being Real holds x ** A is Interval
proof
let A be non empty Interval; ::_thesis: for x being Real holds x ** A is Interval
let x be Real; ::_thesis: x ** A is Interval
percases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; ::_thesis: x ** A is Interval
hence  x ** A is Interval by Th6; ::_thesis: verum
end;
supposeA1: x <> 0 ; ::_thesis: x ** A is Interval
now__::_thesis:_(_(_A_is_open_interval_&_x_**_A_is_Interval_)_or_(_A_is_closed_interval_&_x_**_A_is_Interval_)_or_(_A_is_right_open_interval_&_(_(_x_<_0_&_x_**_A_is_Interval_)_or_(_0_<_x_&_x_**_A_is_Interval_)_)_)_or_(_A_is_left_open_interval_&_x_**_A_is_Interval_)_)
percases ( A is open_interval or A is closed_interval or A is right_open_interval or A is left_open_interval ) by MEASURE5:1;
case A is open_interval ; ::_thesis: x ** A is Interval
then  x ** A is open_interval by A1, Th7;
hence  x ** A is Interval ; ::_thesis: verum
end;
case A is closed_interval ; ::_thesis: x ** A is Interval
then  x ** A is closed_interval by A1, Th8;
hence  x ** A is Interval ; ::_thesis: verum
end;
caseA2: A is right_open_interval ; ::_thesis: verum
percases ( x < 0 or 0 < x ) by A1;
case x < 0 ; ::_thesis: x ** A is Interval
then  x ** A is left_open_interval by A2, Th10;
hence  x ** A is Interval ; ::_thesis: verum
end;
case 0 < x ; ::_thesis: x ** A is Interval
then  x ** A is right_open_interval by A2, Th9;
hence  x ** A is Interval ; ::_thesis: verum
end;
end;
end;
caseA3: A is left_open_interval ; ::_thesis: x ** A is Interval
now__::_thesis:_(_(_x_<_0_&_x_**_A_is_Interval_)_or_(_0_<_x_&_x_**_A_is_Interval_)_)
percases ( x < 0 or 0 < x ) by A1;
case x < 0 ; ::_thesis: x ** A is Interval
then  x ** A is right_open_interval by A3, Th12;
hence  x ** A is Interval ; ::_thesis: verum
end;
case 0 < x ; ::_thesis: x ** A is Interval
then  x ** A is left_open_interval by A3, Th11;
hence  x ** A is Interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is Interval ; ::_thesis: verum
end;
end;
end;
hence  x ** A is Interval ; ::_thesis: verum
end;
end;
end;

registration
let A be interval Subset of REAL;
let x be Real;
clusterx ** A ->  interval ;
correctness
coherence
x ** A is interval ;
proof
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: x ** A is interval
hence  x ** A is interval ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: x ** A is interval
hence  x ** A is interval by Th17; ::_thesis: verum
end;
end;
end;
end;

Lm1:  for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_above holds
A is bounded_above
proof
let A be non empty Subset of REAL; ::_thesis: for x being Real st x > 0 & x ** A is bounded_above holds
A is bounded_above
let x be Real; ::_thesis: ( x > 0 & x ** A is bounded_above implies A is bounded_above )
assume that
A1: x > 0 and
A2: x ** A is bounded_above ; ::_thesis: A is bounded_above
A3: sup (x ** A) <> +infty by A2;
consider r being real number  such that
A4: r in A by MEMBERED:9;
percases ( sup (x ** A) = -infty or sup (x ** A) in REAL ) by A3, XXREAL_0:14;
supposeA5: sup (x ** A) = -infty ; ::_thesis: A is bounded_above
take  0 ; :: according to XXREAL_2:def_10 ::_thesis: 0 is UpperBound of A
A6: x * r in x ** A by A4, MEMBER_1:193;
 -infty is UpperBound of x ** A by A5, XXREAL_2:def_3;
hence  0 is UpperBound of A by A6, XXREAL_0:6, XXREAL_2:def_1; ::_thesis: verum
end;
suppose sup (x ** A) in REAL ; ::_thesis: A is bounded_above
then reconsider r = sup (x ** A) as Real ;
take  r / x ; :: according to XXREAL_2:def_10 ::_thesis: r / x is UpperBound of A
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not z in A or z <= r / x )
assume A7: z in A ; ::_thesis: z <= r / x
 (x ") ** (x ** A) = A by A1, Th1;
then consider s being Real such that
A8: s in x ** A and
A9: z = (x ") * s by A7, INTEGRA2:39;
 s <= r by A8, XXREAL_2:4;
then  s / x <= r / x by A1, XREAL_1:72;
hence  z <= r / x by A9; ::_thesis: verum
end;
end;
end;

theorem Th18: :: URYSOHN2:18
for A being non empty Subset of REAL
for x being Real
for y being R_eal st x = y & 0 <= y holds
sup (x ** A) = y * (sup A)
proof
let A be non empty Subset of REAL; ::_thesis: for x being Real
for y being R_eal st x = y & 0 <= y holds
sup (x ** A) = y * (sup A)
let x be Real; ::_thesis: for y being R_eal st x = y & 0 <= y holds
sup (x ** A) = y * (sup A)
let y be R_eal; ::_thesis: ( x = y & 0 <= y implies sup (x ** A) = y * (sup A) )
assume that
A1: x = y and
A2: 0 <= y ; ::_thesis: sup (x ** A) = y * (sup A)
reconsider Y = x ** A as non empty Subset of REAL ;
percases ( not A is bounded_above or A is bounded_above ) ;
supposeA3: not A is bounded_above ; ::_thesis: sup (x ** A) = y * (sup A)
percases ( y = 0 or y > 0 ) by A2;
supposeA4: y = 0 ; ::_thesis: sup (x ** A) = y * (sup A)
then  x ** A = {0} by A1, INTEGRA2:40;
hence  sup (x ** A) = 0 by XXREAL_2:11
.= y * (sup A) by A4 ;
::_thesis: verum
end;
supposeA5: y > 0 ; ::_thesis: sup (x ** A) = y * (sup A)
then  not Y is bounded_above by A1, A3, Lm1;
hence  sup (x ** A) = +infty by XXREAL_2:73
.= y * +infty by A5, XXREAL_3:def_5
.= y * (sup A) by A3, XXREAL_2:73 ;
::_thesis: verum
end;
end;
end;
suppose A is bounded_above ; ::_thesis: sup (x ** A) = y * (sup A)
then reconsider X = A as non empty real-membered bounded_above set ;
reconsider u = upper_bound X as Real by XREAL_0:def_1;
 x ** X is bounded_above by A1, A2, INTEGRA2:9;
then reconsider Y = Y as non empty real-membered bounded_above set ;
thus  sup (x ** A) = upper_bound Y
.= x * u by A1, A2, INTEGRA2:13
.= y * (sup A) by A1, EXTREAL1:1 ; ::_thesis: verum
end;
end;
end;

Lm2:  for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_below holds
A is bounded_below
proof
let A be non empty Subset of REAL; ::_thesis: for x being Real st x > 0 & x ** A is bounded_below holds
A is bounded_below
let x be Real; ::_thesis: ( x > 0 & x ** A is bounded_below implies A is bounded_below )
assume that
A1: x > 0 and
A2: x ** A is bounded_below ; ::_thesis: A is bounded_below
A3: inf (x ** A) <> -infty by A2;
consider r being real number  such that
A4: r in A by MEMBERED:9;
percases ( inf (x ** A) = +infty or inf (x ** A) in REAL ) by A3, XXREAL_0:14;
supposeA5: inf (x ** A) = +infty ; ::_thesis: A is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of A
A6: x * r in x ** A by A4, MEMBER_1:193;
 +infty is LowerBound of x ** A by A5, XXREAL_2:def_4;
hence  0 is LowerBound of A by A6, XXREAL_0:4, XXREAL_2:def_2; ::_thesis: verum
end;
suppose inf (x ** A) in REAL ; ::_thesis: A is bounded_below
then reconsider r = inf (x ** A) as Real ;
take  r / x ; :: according to XXREAL_2:def_9 ::_thesis: r / x is LowerBound of A
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not z in A or r / x <= z )
assume A7: z in A ; ::_thesis: r / x <= z
 (x ") ** (x ** A) = A by A1, Th1;
then consider s being Real such that
A8: s in x ** A and
A9: z = (x ") * s by A7, INTEGRA2:39;
 r / x <= s / x by A1, A8, XREAL_1:72, XXREAL_2:3;
hence  r / x <= z by A9; ::_thesis: verum
end;
end;
end;

theorem Th19: :: URYSOHN2:19
for A being non empty Subset of REAL
for x being Real
for y being R_eal st x = y & 0 <= y holds
inf (x ** A) = y * (inf A)
proof
let A be non empty Subset of REAL; ::_thesis: for x being Real
for y being R_eal st x = y & 0 <= y holds
inf (x ** A) = y * (inf A)
let x be Real; ::_thesis: for y being R_eal st x = y & 0 <= y holds
inf (x ** A) = y * (inf A)
let y be R_eal; ::_thesis: ( x = y & 0 <= y implies inf (x ** A) = y * (inf A) )
assume that
A1: x = y and
A2: 0 <= y ; ::_thesis: inf (x ** A) = y * (inf A)
reconsider Y = x ** A as non empty Subset of REAL ;
percases ( not A is bounded_below or A is bounded_below ) ;
supposeA3: not A is bounded_below ; ::_thesis: inf (x ** A) = y * (inf A)
percases ( y = 0 or y > 0 ) by A2;
supposeA4: y = 0 ; ::_thesis: inf (x ** A) = y * (inf A)
then  x ** A = {0} by A1, INTEGRA2:40;
hence  inf (x ** A) = 0 by XXREAL_2:13
.= y * (inf A) by A4 ;
::_thesis: verum
end;
supposeA5: y > 0 ; ::_thesis: inf (x ** A) = y * (inf A)
then  not Y is bounded_below by A1, A3, Lm2;
hence  inf (x ** A) = -infty by XXREAL_2:74
.= y * -infty by A5, XXREAL_3:def_5
.= y * (inf A) by A3, XXREAL_2:74 ;
::_thesis: verum
end;
end;
end;
suppose A is bounded_below ; ::_thesis: inf (x ** A) = y * (inf A)
then reconsider X = A as non empty real-membered bounded_below set ;
reconsider u = lower_bound X as Real by XREAL_0:def_1;
 x ** X is bounded_below by A1, A2, INTEGRA2:11;
then reconsider Y = Y as non empty real-membered bounded_below set ;
thus  inf (x ** A) = lower_bound Y
.= x * u by A1, A2, INTEGRA2:15
.= y * (inf A) by A1, EXTREAL1:1 ; ::_thesis: verum
end;
end;
end;

theorem :: URYSOHN2:20
for A being Interval
for x being Real st 0 <= x holds
for y being Real st y = diameter A holds
x * y = diameter (x ** A)
proof
let A be Interval; ::_thesis: for x being Real st 0 <= x holds
for y being Real st y = diameter A holds
x * y = diameter (x ** A)
let x be Real; ::_thesis: ( 0 <= x implies for y being Real st y = diameter A holds
x * y = diameter (x ** A) )
assume A1: 0 <= x ; ::_thesis: for y being Real st y = diameter A holds
x * y = diameter (x ** A)
let y be Real; ::_thesis: ( y = diameter A implies x * y = diameter (x ** A) )
assume A2: y = diameter A ; ::_thesis: x * y = diameter (x ** A)
percases ( A is empty or not A is empty ) ;
supposeA3: A is empty ; ::_thesis: x * y = diameter (x ** A)
then A4: x ** A is empty ;
thus x * y = 0 by A2, A3, MEASURE5:10
.= diameter (x ** A) by A4, MEASURE5:10 ; ::_thesis: verum
end;
supposeA6: not A is empty ; ::_thesis: x * y = diameter (x ** A)
then consider z being real number  such that
A7: z in A by MEMBERED:9;
reconsider z = z as Real by XREAL_0:def_1;
A8: x * z in x ** A by A7, MEMBER_1:193;
reconsider AA = A as non empty Subset of REAL by A6;
reconsider u = x as R_eal by XXREAL_0:def_1;
A9: inf (x ** AA) = u * (inf AA) by A1, Th19;
reconsider z = x as R_eal by XXREAL_0:def_1;
thus x * y = z * (diameter A) by A2, EXTREAL1:1
.= z * ((sup A) - (inf A)) by A6, MEASURE5:def_6
.= (z * (sup A)) - (z * (inf A)) by XXREAL_3:100
.= (sup (x ** A)) - (inf (x ** A)) by A1, A9, Th18
.= diameter (x ** A) by A8, MEASURE5:def_6 ; ::_thesis: verum
end;
end;
end;

theorem Th21: :: URYSOHN2:21
for eps being Real st 0 < eps holds
ex n being Element of NAT st 1 < (2 |^ n) * eps
proof
let eps be Real; ::_thesis: ( 0 < eps implies ex n being Element of NAT st 1 < (2 |^ n) * eps )
assume A1: 0 < eps ; ::_thesis: ex n being Element of NAT st 1 < (2 |^ n) * eps
consider n being Element of NAT  such that
A2: 1 / eps < n by SEQ_4:3;
take  n ; ::_thesis: 1 < (2 |^ n) * eps
 1 / eps < 2 |^ n by A2, NEWTON:86, XXREAL_0:2;
then  (1 / eps) * eps < (2 |^ n) * eps by A1, XREAL_1:68;
hence  1 < (2 |^ n) * eps by A1, XCMPLX_1:87; ::_thesis: verum
end;

theorem Th22: :: URYSOHN2:22
for a, b being Real st 0 <= a & 1 < b - a holds
ex n being Element of NAT st
( a < n & n < b )
proof
let a, b be Real; ::_thesis: ( 0 <= a & 1 < b - a implies ex n being Element of NAT st
( a < n & n < b ) )
assume that
A1: 0 <= a and
A2: 1 < b - a ; ::_thesis: ex n being Element of NAT st
( a < n & n < b )
 a < [\a/] + 1 by INT_1:29;
then reconsider n = [\a/] + 1 as Element of NAT by A1, INT_1:3;
take  n ; ::_thesis: ( a < n & n < b )
thus  a < n by INT_1:29; ::_thesis: n < b
 [\a/] <= a by INT_1:def_6;
then A3: [\a/] + 1 <= a + 1 by XREAL_1:6;
 1 + a < b by A2, XREAL_1:20;
hence  n < b by A3, XXREAL_0:2; ::_thesis: verum
end;

theorem :: URYSOHN2:23
for n being Element of NAT holds dyadic n c= DYADIC
proof
let n be Element of NAT ; ::_thesis: dyadic n c= DYADIC
 for x being set st x in dyadic n holds
x in DYADIC by URYSOHN1:def_2;
hence  dyadic n c= DYADIC by TARSKI:def_3; ::_thesis: verum
end;

theorem Th24: :: URYSOHN2:24
for a, b being Real st a < b & 0 <= a & b <= 1 holds
ex c being Real st
( c in DYADIC & a < c & c < b )
proof
let a, b be Real; ::_thesis: ( a < b & 0 <= a & b <= 1 implies ex c being Real st
( c in DYADIC & a < c & c < b ) )
assume that
A1: a < b and
A2: 0 <= a and
A3: b <= 1 ; ::_thesis: ex c being Real st
( c in DYADIC & a < c & c < b )
set eps = b - a;
consider n being Element of NAT  such that
A4: 1 < (2 |^ n) * (b - a) by A1, Th21, XREAL_1:50;
set aa = (2 |^ n) * a;
set bb = (2 |^ n) * b;
 1 < ((2 |^ n) * b) - ((2 |^ n) * a) by A4;
then consider m being Element of NAT  such that
A5: (2 |^ n) * a < m and
A6: m < (2 |^ n) * b by A2, Th22;
set x = m / (2 |^ n);
take  m / (2 |^ n) ; ::_thesis: ( m / (2 |^ n) in DYADIC & a < m / (2 |^ n) & m / (2 |^ n) < b )
A7: 0 < 2 |^ n by NEWTON:83;
 m / (2 |^ n) < b by A6, NEWTON:83, XREAL_1:83;
then  m / (2 |^ n) < 1 by A3, XXREAL_0:2;
then  m < 2 |^ n by A7, XREAL_1:181;
then  m / (2 |^ n) in dyadic n by URYSOHN1:def_1;
hence  ( m / (2 |^ n) in DYADIC & a < m / (2 |^ n) & m / (2 |^ n) < b ) by A7, A5, A6, URYSOHN1:def_2, XREAL_1:81, XREAL_1:83; ::_thesis: verum
end;

theorem Th25: :: URYSOHN2:25
for a, b being Real st a < b holds
ex c being Real st
( c in DOM & a < c & c < b )
proof
let a, b be Real; ::_thesis: ( a < b implies ex c being Real st
( c in DOM & a < c & c < b ) )
assume A1: a < b ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
percases ( ( a < 0 & b <= 1 ) or ( a < 0 & 1 < b ) or ( 0 <= a & b <= 1 ) or ( 0 <= a & 1 < b ) ) ;
supposeA2: ( a < 0 & b <= 1 ) ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
now__::_thesis:_(_(_b_<=_0_&_ex_c_being_Real_st_
(_c_in_DOM_&_a_<_c_&_c_<_b_)_)_or_(_0_<_b_&_ex_c_being_Real_st_
(_c_in_DOM_&_a_<_c_&_c_<_b_)_)_)
percases ( b <= 0 or 0 < b ) ;
caseA3: b <= 0 ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
consider c being real number  such that
A4: a < c and
A5: c < b by A1, XREAL_1:5;
reconsider c = c as Real by XREAL_0:def_1;
 halfline 0 =  {  g where g is Real : g < 0  }  by XXREAL_1:229;
then  c in halfline 0 by A3, A5;
then  c in (halfline 0) \/ DYADIC by XBOOLE_0:def_3;
then  c in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
hence  ex c being Real st
( c in DOM & a < c & c < b ) by A4, A5; ::_thesis: verum
end;
caseA6: 0 < b ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
set a1 = 0 ;
consider c being Real such that
A7: c in DYADIC and
A8: ( 0 < c & c < b ) by A2, A6, Th24;
 c in (halfline 0) \/ DYADIC by A7, XBOOLE_0:def_3;
then  c in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
hence  ex c being Real st
( c in DOM & a < c & c < b ) by A2, A8; ::_thesis: verum
end;
end;
end;
hence  ex c being Real st
( c in DOM & a < c & c < b ) ; ::_thesis: verum
end;
supposeA9: ( a < 0 & 1 < b ) ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
consider a1, b1 being Real such that
A10: ( a1 = 0 & b1 = 1 ) ;
consider c being Real such that
A11: c in DYADIC and
A12: ( a1 < c & c < b1 ) by A10, Th24;
take  c ; ::_thesis: ( c in DOM & a < c & c < b )
 c in (halfline 0) \/ DYADIC by A11, XBOOLE_0:def_3;
hence  ( c in DOM & a < c & c < b ) by A9, A10, A12, URYSOHN1:def_3, XBOOLE_0:def_3, XXREAL_0:2; ::_thesis: verum
end;
suppose ( 0 <= a & b <= 1 ) ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
then consider c being Real such that
A13: c in DYADIC and
A14: ( a < c & c < b ) by A1, Th24;
take  c ; ::_thesis: ( c in DOM & a < c & c < b )
 c in (halfline 0) \/ DYADIC by A13, XBOOLE_0:def_3;
hence  ( c in DOM & a < c & c < b ) by A14, URYSOHN1:def_3, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA15: ( 0 <= a & 1 < b ) ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
now__::_thesis:_(_(_1_<=_a_&_ex_c_being_Real_st_
(_c_in_DOM_&_a_<_c_&_c_<_b_)_)_or_(_a_<_1_&_ex_c_being_Real_st_
(_c_in_DOM_&_a_<_c_&_c_<_b_)_)_)
percases ( 1 <= a or a < 1 ) ;
caseA16: 1 <= a ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
consider c being real number  such that
A17: a < c and
A18: c < b by A1, XREAL_1:5;
reconsider c = c as Real by XREAL_0:def_1;
 ( right_open_halfline 1 =  {  g where g is Real : 1 < g  }  & 1 < c ) by A16, A17, XXREAL_0:2, XXREAL_1:230;
then  c in right_open_halfline 1 ;
then  c in DYADIC \/ (right_open_halfline 1) by XBOOLE_0:def_3;
then  c in (halfline 0) \/ (DYADIC \/ (right_open_halfline 1)) by XBOOLE_0:def_3;
then  c in DOM by URYSOHN1:def_3, XBOOLE_1:4;
hence  ex c being Real st
( c in DOM & a < c & c < b ) by A17, A18; ::_thesis: verum
end;
caseA19: a < 1 ; ::_thesis: ex c being Real st
( c in DOM & a < c & c < b )
set b1 = 1;
consider c being Real such that
A20: c in DYADIC and
A21: a < c and
A22: c < 1 by A15, A19, Th24;
 c in (halfline 0) \/ DYADIC by A20, XBOOLE_0:def_3;
then A23: c in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
 c < b by A15, A22, XXREAL_0:2;
hence  ex c being Real st
( c in DOM & a < c & c < b ) by A21, A23; ::_thesis: verum
end;
end;
end;
hence  ex c being Real st
( c in DOM & a < c & c < b ) ; ::_thesis: verum
end;
end;
end;

theorem :: URYSOHN2:26
for A being non empty Subset of ExtREAL
for a, b being R_eal st A c= [.a,b.] holds
( a <= inf A & sup A <= b )
proof
let A be non empty Subset of ExtREAL; ::_thesis: for a, b being R_eal st A c= [.a,b.] holds
( a <= inf A & sup A <= b )
let a, b be R_eal; ::_thesis: ( A c= [.a,b.] implies ( a <= inf A & sup A <= b ) )
assume A1: A c= [.a,b.] ; ::_thesis: ( a <= inf A & sup A <= b )
then reconsider B = [.a,b.] as non empty Subset of ExtREAL by MEMBERED:2;
 for x being ext-real number st x in B holds
x <= b by XXREAL_1:1;
then  b is UpperBound of B by XXREAL_2:def_1;
then A2: b is UpperBound of A by A1, XXREAL_2:6;
 for x being ext-real number st x in B holds
a <= x by XXREAL_1:1;
then  a is LowerBound of B by XXREAL_2:def_2;
then  a is LowerBound of A by A1, XXREAL_2:5;
hence  ( a <= inf A & sup A <= b ) by A2, XXREAL_2:def_3, XXREAL_2:def_4; ::_thesis: verum
end;

theorem :: URYSOHN2:27
( 0 in DYADIC & 1 in DYADIC )
proof
 ( 0 in dyadic 0 & 1 in dyadic 0 ) by URYSOHN1:6;
hence  ( 0 in DYADIC & 1 in DYADIC ) by URYSOHN1:def_2; ::_thesis: verum
end;

theorem :: URYSOHN2:28
DYADIC c= [.0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in DYADIC or x in [.0,1.] )
assume A1: x in DYADIC ; ::_thesis: x in [.0,1.]
then reconsider x = x as Real ;
A2: ex n being Element of NAT st x in dyadic n by A1, URYSOHN1:def_2;
reconsider x = x as R_eal by XXREAL_0:def_1;
 ( 0 <= x & x <= 1 ) by A2, URYSOHN1:1;
hence  x in [.0,1.] by XXREAL_1:1; ::_thesis: verum
end;

theorem :: URYSOHN2:29
for n, k being Element of NAT st n <= k holds
dyadic n c= dyadic k
proof
let n, k be Element of NAT ; ::_thesis: ( n <= k implies dyadic n c= dyadic k )
A1: for s being Element of NAT holds dyadic n c= dyadic (n + s)
proof
defpred S1[ Element of NAT ] means  dyadic n c= dyadic (n + $1);
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A3: dyadic (n + k) c= dyadic ((n + k) + 1) by URYSOHN1:5;
assume  dyadic n c= dyadic (n + k) ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
A4: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2);
hence  for s being Element of NAT holds dyadic n c= dyadic (n + s) ; ::_thesis: verum
end;
assume  n <= k ; ::_thesis: dyadic n c= dyadic k
then consider s being Nat such that
A5: k = n + s by NAT_1:10;
 s in NAT by ORDINAL1:def_12;
hence  dyadic n c= dyadic k by A1, A5; ::_thesis: verum
end;

theorem Th30: :: URYSOHN2:30
for a, b, c, d being Real st a < c & c < b & a < d & d < b holds
abs (d - c) < b - a
proof
let a, b, c, d be Real; ::_thesis: ( a < c & c < b & a < d & d < b implies abs (d - c) < b - a )
assume that
A1: a < c and
A2: ( c < b & a < d ) and
A3: d < b ; ::_thesis: abs (d - c) < b - a
A4: c + a < b + d by A2, XREAL_1:8;
then  c - d <= b - a by XREAL_1:21;
then A5: - (b - a) <= - (c - d) by XREAL_1:24;
A6: a + d < c + b by A1, A3, XREAL_1:8;
A7: abs (d - c) <> b - a
proof
assume A8: abs (d - c) = b - a ; ::_thesis: contradiction
A9: ( d - c = b - a or d - c = - (b - a) )
proof
percases ( 0 <= d - c or not 0 <= d - c ) ;
suppose 0 <= d - c ; ::_thesis: ( d - c = b - a or d - c = - (b - a) )
hence  ( d - c = b - a or d - c = - (b - a) ) by A8, ABSVALUE:def_1; ::_thesis: verum
end;
suppose not 0 <= d - c ; ::_thesis: ( d - c = b - a or d - c = - (b - a) )
then  b - a = - (d - c) by A8, ABSVALUE:def_1;
hence  ( d - c = b - a or d - c = - (b - a) ) ; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_(_d_-_c_=_b_-_a_&_contradiction_)_or_(_d_-_c_=_-_(b_-_a)_&_contradiction_)_)
percases ( d - c = b - a or d - c = - (b - a) ) by A9;
case d - c = b - a ; ::_thesis: contradiction
hence  contradiction by A6; ::_thesis: verum
end;
case d - c = - (b - a) ; ::_thesis: contradiction
hence  contradiction by A4; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
 d - c < b - a by A6, XREAL_1:21;
then  abs (d - c) <= b - a by A5, ABSVALUE:5;
hence  abs (d - c) < b - a by A7, XXREAL_0:1; ::_thesis: verum
end;

theorem :: URYSOHN2:31
for eps being Real st 0 < eps holds
for d being Real st 0 < d holds
ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
proof
let eps be Real; ::_thesis: ( 0 < eps implies for d being Real st 0 < d holds
ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) )
assume  0 < eps ; ::_thesis: for d being Real st 0 < d holds
ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
then consider eps1 being real number  such that
A1: 0 < eps1 and
A2: eps1 < eps by XREAL_1:5;
reconsider eps1 = eps1 as Real by XREAL_0:def_1;
let d be Real; ::_thesis: ( 0 < d implies ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) )
assume A3: 0 < d ; ::_thesis: ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
percases ( eps1 < d or d <= eps1 ) ;
suppose eps1 < d ; ::_thesis: ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
then A4: 0 < d - eps1 by XREAL_1:50;
 d - eps1 < d - 0 by A1, XREAL_1:15;
then  ex c being Real st
( c in DOM & d - eps1 < c & c < d ) by Th25;
then consider r1 being Real such that
A5: d - eps1 < r1 and
A6: r1 < d and
A7: r1 in DOM ;
 ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by A7, URYSOHN1:def_3, XBOOLE_0:def_3;
then A8: ( r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def_3;
 eps - eps < eps - eps1 by A2, XREAL_1:15;
then  d + 0 < d + (eps - eps1) by XREAL_1:8;
then  ex c being Real st
( c in DOM & d < c & c < d + (eps - eps1) ) by Th25;
then consider r2 being Real such that
A9: d < r2 and
A10: r2 < d + (eps - eps1) and
A11: r2 in DOM ;
 ( r2 in (halfline 0) \/ DYADIC or r2 in right_open_halfline 1 ) by A11, URYSOHN1:def_3, XBOOLE_0:def_3;
then A12: ( r2 in halfline 0 or r2 in DYADIC or r2 in right_open_halfline 1 ) by XBOOLE_0:def_3;
A13: r1 < r2 by A6, A9, XXREAL_0:2;
then A14: d - eps1 < r2 by A5, XXREAL_0:2;
take  r1 ; ::_thesis: ex r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
take  r2 ; ::_thesis: ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
A15: (d + (eps - eps1)) - (d - eps1) = eps ;
 r1 < d + (eps - eps1) by A10, A13, XXREAL_0:2;
then A16: abs (r2 - r1) < eps by A5, A10, A14, A15, Th30;
 0 <= r2 - r1 by A13, XREAL_1:48;
hence  ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) by A5, A6, A9, A4, A8, A12, A16, ABSVALUE:def_1, XBOOLE_0:def_3, XXREAL_1:233; ::_thesis: verum
end;
supposeA17: d <= eps1 ; ::_thesis: ex r1, r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
consider r1 being Real such that
A18: r1 in DOM and
A19: 0 < r1 and
A20: r1 < d by A3, Th25;
A21: ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by A18, URYSOHN1:def_3, XBOOLE_0:def_3;
 0 + d < r1 + eps1 by A17, A19, XREAL_1:8;
then  ex c being Real st
( c in DOM & d < c & c < r1 + eps1 ) by Th25;
then consider r2 being Real such that
A22: d < r2 and
A23: r2 < r1 + eps1 and
A24: r2 in DOM ;
take  r1 ; ::_thesis: ex r2 being Real st
( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
take  r2 ; ::_thesis: ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )
A25: ( r2 in (halfline 0) \/ DYADIC or r2 in right_open_halfline 1 ) by A24, URYSOHN1:def_3, XBOOLE_0:def_3;
 not r1 in halfline 0 by A19, XXREAL_1:233;
then A26: ( r1 in DYADIC or r1 in right_open_halfline 1 ) by A21, XBOOLE_0:def_3;
 not r2 in halfline 0 by A3, A22, XXREAL_1:233;
then A27: ( r2 in DYADIC or r2 in right_open_halfline 1 ) by A25, XBOOLE_0:def_3;
 r2 - r1 < (r1 + eps1) - r1 by A23, XREAL_1:9;
hence  ( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps ) by A2, A19, A20, A22, A26, A27, XBOOLE_0:def_3, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

begin

theorem :: URYSOHN2:32
for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_above holds
A is bounded_above by Lm1;

theorem :: URYSOHN2:33
for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_below holds
A is bounded_below by Lm2;