:: MEASURE6 semantic presentation

begin

theorem :: MEASURE6:1
ex F being Function of NAT,[:NAT,NAT:] st
( F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:] )
proof
consider F being Function such that
A1: F is one-to-one and
A2: ( dom F = NAT & rng F = [:NAT,NAT:] ) by CARD_4:5, WELLORD2:def_4;
 F is Function of NAT,[:NAT,NAT:] by A2, FUNCT_2:1;
hence  ex F being Function of NAT,[:NAT,NAT:] st
( F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:] ) by A1, A2; ::_thesis: verum
end;

theorem :: MEASURE6:2
for F being Function of NAT,ExtREAL st F is nonnegative holds
0. <= SUM F
proof
let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative implies 0. <= SUM F )
assume  F is nonnegative ; ::_thesis: 0. <= SUM F
then  0. <= (Ser F) . 0 by SUPINF_2:40;
hence  0. <= SUM F by FUNCT_2:4, XXREAL_2:4; ::_thesis: verum
end;

theorem :: MEASURE6:3
for F being Function of NAT,ExtREAL
for x being R_eal st ex n being Element of NAT st x <= F . n & F is nonnegative holds
x <= SUM F
proof
let F be Function of NAT,ExtREAL; ::_thesis: for x being R_eal st ex n being Element of NAT st x <= F . n & F is nonnegative holds
x <= SUM F
let x be R_eal; ::_thesis: ( ex n being Element of NAT st x <= F . n & F is nonnegative implies x <= SUM F )
assume that
A1: ex n being Element of NAT st x <= F . n and
A2: F is nonnegative ; ::_thesis: x <= SUM F
consider n being Element of NAT  such that
A3: x <= F . n by A1;
A4: (Ser F) . n <= SUM F by FUNCT_2:4, XXREAL_2:4;
percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
suppose n = 0 ; ::_thesis: x <= SUM F
then  (Ser F) . n = F . n by SUPINF_2:44;
hence  x <= SUM F by A3, A4, XXREAL_0:2; ::_thesis: verum
end;
suppose ex k being Nat st n = k + 1 ; ::_thesis: x <= SUM F
then consider k being Nat such that
A5: n = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A6: 0. <= (Ser F) . k by A2, SUPINF_2:40;
 (Ser F) . n = ((Ser F) . k) + (F . (k + 1)) by A5, SUPINF_2:44;
then  0. + x <= (Ser F) . n by A3, A5, A6, XXREAL_3:36;
then  x <= (Ser F) . n by XXREAL_3:4;
hence  x <= SUM F by A4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

definition
let x be ext-real number ;
func R_EAL x ->  R_eal equals :: MEASURE6:def 1
x;
coherence
 x is R_eal by XXREAL_0:def_1;
end;

:: deftheorem  defines R_EAL MEASURE6:def_1_:_
 for x being ext-real number holds R_EAL x = x;

theorem :: MEASURE6:4
for eps being R_eal st 0. < eps holds
ex F being Function of NAT,ExtREAL st
( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps )
proof
defpred S1[ set , set , set ] means  for a, b being R_eal
for s being Element of NAT st s = $1 & a = $2 & b = $3 holds
b = a / 2;
let eps be R_eal; ::_thesis: ( 0. < eps implies ex F being Function of NAT,ExtREAL st
( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps ) )
assume  0. < eps ; ::_thesis: ex F being Function of NAT,ExtREAL st
( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps )
then consider x0 being real number  such that
A1: 0. < x0 and
A2: x0 < eps by XXREAL_3:3;
consider x being real number  such that
A3: 0. < x and
A4: x + x < x0 by A1, XXREAL_3:50;
reconsider x = x as Element of ExtREAL by XXREAL_0:def_1;
A5: for n being Element of NAT
for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y]
let x be Element of ExtREAL ; ::_thesis: ex y being Element of ExtREAL st S1[n,x,y]
reconsider m = x / 2 as Element of ExtREAL by XXREAL_0:def_1;
take  m ; ::_thesis: S1[n,x,m]
thus  S1[n,x,m] ; ::_thesis: verum
end;
consider F being Function of NAT,ExtREAL such that
A6: ( F . 0 = x & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A5);
take  F ; ::_thesis: ( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps )
defpred S2[ Element of NAT ] means  0. < F . $1;
A7: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A8: 0. < F . k ; ::_thesis: S2[k + 1]
 F . (k + 1) = (F . k) / 2 by A6;
hence  S2[k + 1] by A8; ::_thesis: verum
end;
A9: S2[ 0 ] by A3, A6;
thus A10: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A9, A7); ::_thesis: SUM F < eps
then  for n being Element of NAT holds 0. <= F . n ;
then A11: F is nonnegative by SUPINF_2:39;
 for s being ext-real number st s in rng (Ser F) holds
s <= x0
proof
defpred S3[ Element of NAT ] means ((Ser F) . $1) + (F . $1) < x0;
let s be ext-real number ; ::_thesis: ( s in rng (Ser F) implies s <= x0 )
assume  s in rng (Ser F) ; ::_thesis: s <= x0
then consider n being set  such that
A12: n in dom (Ser F) and
A13: s = (Ser F) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A12;
A14: for l being Element of NAT st S3[l] holds
S3[l + 1]
proof
let l be Element of NAT ; ::_thesis: ( S3[l] implies S3[l + 1] )
 F . (l + 1) = (F . l) / 2 by A6;
then A15: ((Ser F) . l) + ((F . (l + 1)) + (F . (l + 1))) <= ((Ser F) . l) + (F . l) by XXREAL_3:105;
 ( 0. <= (Ser F) . l & 0. <= F . (l + 1) ) by A10, A11, SUPINF_2:40;
then A16: ( ((Ser F) . (l + 1)) + (F . (l + 1)) = (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) & (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) <= ((Ser F) . l) + (F . l) ) by A15, SUPINF_2:44, XXREAL_3:44;
assume  ((Ser F) . l) + (F . l) < x0 ; ::_thesis: S3[l + 1]
hence  S3[l + 1] by A16, XXREAL_0:2; ::_thesis: verum
end;
A17: S3[ 0 ] by A4, A6, SUPINF_2:44;
 for k being Element of NAT holds S3[k] from NAT_1:sch_1(A17, A14);
then A18: ((Ser F) . n) + (F . n) < x0 ;
 ( 0. <= (Ser F) . n & 0. <= F . n ) by A10, A11, SUPINF_2:40;
hence  s <= x0 by A13, A18, XXREAL_3:48; ::_thesis: verum
end;
then  x0 is UpperBound of rng (Ser F) by XXREAL_2:def_1;
then A19: sup (rng (Ser F)) <= x0 by XXREAL_2:def_3;
percases ( SUM F < x0 or SUM F = x0 ) by A19, XXREAL_0:1;
suppose SUM F < x0 ; ::_thesis: SUM F < eps
hence  SUM F < eps by A2, XXREAL_0:2; ::_thesis: verum
end;
suppose SUM F = x0 ; ::_thesis: SUM F < eps
hence  SUM F < eps by A2; ::_thesis: verum
end;
end;
end;

theorem :: MEASURE6:5
for eps being R_eal
for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds
ex x being ext-real number st
( x in X & x < (inf X) + eps )
proof
let eps be R_eal; ::_thesis: for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds
ex x being ext-real number st
( x in X & x < (inf X) + eps )
let X be non empty Subset of ExtREAL; ::_thesis: ( 0. < eps & inf X is Real implies ex x being ext-real number st
( x in X & x < (inf X) + eps ) )
assume that
A1: 0. < eps and
A2: inf X is Real ; ::_thesis: ex x being ext-real number st
( x in X & x < (inf X) + eps )
assume  for x being ext-real number holds
( not x in X or not x < (inf X) + eps ) ; ::_thesis: contradiction
then  (inf X) + eps is LowerBound of X by XXREAL_2:def_2;
then A3: (inf X) + eps <= inf X by XXREAL_2:def_4;
percases ( eps < +infty or eps = +infty ) by XXREAL_0:4;
suppose eps < +infty ; ::_thesis: contradiction
then reconsider a = inf X, b = eps as Real by A1, A2, XXREAL_0:48;
 (inf X) + eps = a + b by SUPINF_2:1;
then  b <= a - a by A3, XREAL_1:19;
hence  contradiction by A1; ::_thesis: verum
end;
suppose eps = +infty ; ::_thesis: contradiction
then  (inf X) + eps = +infty by A2, XXREAL_3:def_2;
hence  contradiction by A2, A3, XXREAL_0:4; ::_thesis: verum
end;
end;
end;

theorem :: MEASURE6:6
for eps being R_eal
for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds
ex x being ext-real number st
( x in X & (sup X) - eps < x )
proof
let eps be R_eal; ::_thesis: for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds
ex x being ext-real number st
( x in X & (sup X) - eps < x )
let X be non empty Subset of ExtREAL; ::_thesis: ( 0. < eps & sup X is Real implies ex x being ext-real number st
( x in X & (sup X) - eps < x ) )
assume that
A1: 0. < eps and
A2: sup X is Real ; ::_thesis: ex x being ext-real number st
( x in X & (sup X) - eps < x )
assume  for x being ext-real number holds
( not x in X or not (sup X) - eps < x ) ; ::_thesis: contradiction
then  (sup X) - eps is UpperBound of X by XXREAL_2:def_1;
then A3: sup X <= (sup X) - eps by XXREAL_2:def_3;
percases ( eps < +infty or eps = +infty ) by XXREAL_0:4;
suppose eps < +infty ; ::_thesis: contradiction
then reconsider a = sup X, b = eps as Real by A1, A2, XXREAL_0:48;
 a <= a - b by A3, SUPINF_2:3;
hence  contradiction by A1, XREAL_1:44; ::_thesis: verum
end;
suppose eps = +infty ; ::_thesis: contradiction
then  (sup X) - eps = -infty by A2, XXREAL_3:13;
hence  contradiction by A2, A3, XXREAL_0:6; ::_thesis: verum
end;
end;
end;

theorem :: MEASURE6:7
for F being Function of NAT,ExtREAL st F is nonnegative & SUM F < +infty holds
for n being Element of NAT holds F . n in REAL
proof
let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative & SUM F < +infty implies for n being Element of NAT holds F . n in REAL )
assume that
A1: F is nonnegative and
A2: SUM F < +infty ; ::_thesis: for n being Element of NAT holds F . n in REAL
let n be Element of NAT ; ::_thesis: F . n in REAL
defpred S1[ Element of NAT ] means F . $1 <= (Ser F) . $1;
A3: 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] )
assume  F . k <= (Ser F) . k ; ::_thesis: S1[k + 1]
reconsider x = (Ser F) . k as R_eal ;
 x + (F . (k + 1)) = (Ser F) . (k + 1) by SUPINF_2:44;
hence  S1[k + 1] by A1, SUPINF_2:40, XXREAL_3:39; ::_thesis: verum
end;
A4: S1[ 0 ] by SUPINF_2:44;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
then A5: F . n <= (Ser F) . n ;
 (Ser F) . n <= SUM F by FUNCT_2:4, XXREAL_2:4;
then  F . n <= SUM F by A5, XXREAL_0:2;
then A6: F . n < +infty by A2, XXREAL_0:2;
 ( 0. = 0 & 0. <= F . n ) by A1, SUPINF_2:39;
hence  F . n in REAL by A6, XXREAL_0:46; ::_thesis: verum
end;

registration
cluster non empty complex-membered ext-real-membered real-membered interval for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty & b1 is interval )
proof
take  [#] REAL ; ::_thesis: ( not [#] REAL is empty & [#] REAL is interval )
thus  ( not [#] REAL is empty & [#] REAL is interval ) ; ::_thesis: verum
end;
end;

theorem :: MEASURE6:8
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b & A = ].a,b.[ ) holds
a = inf A by XXREAL_1:28, XXREAL_2:28;

theorem :: MEASURE6:9
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b & A = ].a,b.] ) holds
a = inf A by XXREAL_1:26, XXREAL_2:27;

theorem :: MEASURE6:10
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b & A = [.a,b.] ) holds
a = inf A by XXREAL_2:25;

theorem Th11: :: MEASURE6:11
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b & A = [.a,b.[ ) holds
a = inf A
proof
let A be non empty Interval; ::_thesis: for a being R_eal st ex b being R_eal st
( a <= b & A = [.a,b.[ ) holds
a = inf A
let IT be R_eal; ::_thesis: ( ex b being R_eal st
( IT <= b & A = [.IT,b.[ ) implies IT = inf A )
given b being R_eal such that A1: IT <= b and
A2: A = [.IT,b.[ ; ::_thesis: IT = inf A
 IT <> b by A2;
then  IT < b by A1, XXREAL_0:1;
hence  IT = inf A by A2, XXREAL_2:26; ::_thesis: verum
end;

theorem :: MEASURE6:12
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b & A = ].a,b.[ ) holds
b = sup A by XXREAL_1:28, XXREAL_2:32;

theorem Th13: :: MEASURE6:13
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b & A = ].a,b.] ) holds
b = sup A
proof
let A be non empty Interval; ::_thesis: for b being R_eal st ex a being R_eal st
( a <= b & A = ].a,b.] ) holds
b = sup A
let IT be R_eal; ::_thesis: ( ex a being R_eal st
( a <= IT & A = ].a,IT.] ) implies IT = sup A )
given a being R_eal such that A1: a <= IT and
A2: A = ].a,IT.] ; ::_thesis: IT = sup A
 a <> IT by A2;
then  a < IT by A1, XXREAL_0:1;
hence  IT = sup A by A2, XXREAL_2:30; ::_thesis: verum
end;

theorem :: MEASURE6:14
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b & A = [.a,b.] ) holds
b = sup A by XXREAL_2:29;

theorem Th15: :: MEASURE6:15
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b & A = [.a,b.[ ) holds
b = sup A
proof
let A be non empty Interval; ::_thesis: for b being R_eal st ex a being R_eal st
( a <= b & A = [.a,b.[ ) holds
b = sup A
let IT be R_eal; ::_thesis: ( ex a being R_eal st
( a <= IT & A = [.a,IT.[ ) implies IT = sup A )
given a being R_eal such that A1: a <= IT and
A2: A = [.a,IT.[ ; ::_thesis: IT = sup A
 a <> IT by A2;
then  a < IT by A1, XXREAL_0:1;
hence  IT = sup A by A2, XXREAL_2:31; ::_thesis: verum
end;

theorem :: MEASURE6:16
for A being non empty Interval st A is open_interval holds
A = ].(inf A),(sup A).[
proof
let A be non empty Interval; ::_thesis: ( A is open_interval implies A = ].(inf A),(sup A).[ )
assume  A is open_interval ; ::_thesis: A = ].(inf A),(sup A).[
then consider a, b being R_eal such that
A1: A = ].a,b.[ by MEASURE5:def_2;
 sup A = b by A1, XXREAL_1:28, XXREAL_2:32;
hence  A = ].(inf A),(sup A).[ by A1, XXREAL_1:28, XXREAL_2:28; ::_thesis: verum
end;

theorem :: MEASURE6:17
for A being non empty Interval st A is closed_interval holds
A = [.(inf A),(sup A).]
proof
let A be non empty Interval; ::_thesis: ( A is closed_interval implies A = [.(inf A),(sup A).] )
assume  A is closed_interval ; ::_thesis: A = [.(inf A),(sup A).]
then consider a, b being real number  such that
A1: A = [.a,b.] by MEASURE5:def_3;
A2: a <= b by A1, XXREAL_1:29;
reconsider b = b as R_eal by XXREAL_0:def_1;
 sup A = b by A1, A2, XXREAL_2:29;
hence  A = [.(inf A),(sup A).] by A1, A2, XXREAL_2:25; ::_thesis: verum
end;

theorem :: MEASURE6:18
for A being non empty Interval st A is right_open_interval holds
A = [.(inf A),(sup A).[
proof
let A be non empty Interval; ::_thesis: ( A is right_open_interval implies A = [.(inf A),(sup A).[ )
assume  A is right_open_interval ; ::_thesis: A = [.(inf A),(sup A).[
then consider a being real number , b being R_eal such that
A1: A = [.a,b.[ by MEASURE5:def_4;
reconsider a = a as R_eal by XXREAL_0:def_1;
A2: a <= b by A1, XXREAL_1:27;
then  sup A = b by A1, Th15;
hence  A = [.(inf A),(sup A).[ by A1, A2, Th11; ::_thesis: verum
end;

theorem :: MEASURE6:19
for A being non empty Interval st A is left_open_interval holds
A = ].(inf A),(sup A).]
proof
let A be non empty Interval; ::_thesis: ( A is left_open_interval implies A = ].(inf A),(sup A).] )
assume  A is left_open_interval ; ::_thesis: A = ].(inf A),(sup A).]
then consider a being R_eal, b being real number  such that
A1: A = ].a,b.] by MEASURE5:def_5;
A2: a <= b by A1, XXREAL_1:26;
reconsider b = b as R_eal by XXREAL_0:def_1;
 sup A = b by A2, A1, Th13;
hence  A = ].(inf A),(sup A).] by A1, XXREAL_1:26, XXREAL_2:27; ::_thesis: verum
end;

theorem :: MEASURE6:20
for A, B being non empty Interval
for a, b being real number st a in A & b in B & sup A <= inf B holds
a <= b
proof
let A, B be non empty Interval; ::_thesis: for a, b being real number st a in A & b in B & sup A <= inf B holds
a <= b
let a, b be real number ; ::_thesis: ( a in A & b in B & sup A <= inf B implies a <= b )
assume that
A1: a in A and
A2: b in B ; ::_thesis: ( not sup A <= inf B or a <= b )
A3: inf B <= R_EAL b by A2, XXREAL_2:3;
assume A4: sup A <= inf B ; ::_thesis: a <= b
 R_EAL a <= sup A by A1, XXREAL_2:4;
then  R_EAL a <= inf B by A4, XXREAL_0:2;
hence  a <= b by A3, XXREAL_0:2; ::_thesis: verum
end;

theorem :: MEASURE6:21
for A, B being real-membered set
for y being Real holds
( y in B ++ A iff ex x, z being Real st
( x in B & z in A & y = x + z ) )
proof
let A, B be real-membered set ; ::_thesis: for y being Real holds
( y in B ++ A iff ex x, z being Real st
( x in B & z in A & y = x + z ) )
let y be Real; ::_thesis: ( y in B ++ A iff ex x, z being Real st
( x in B & z in A & y = x + z ) )
hereby  ::_thesis: ( ex x, z being Real st
( x in B & z in A & y = x + z ) implies y in B ++ A )
assume  y in B ++ A ; ::_thesis: ex x, w being Element of REAL st
( x in B & w in A & y = x + w )
then consider x, w being Element of COMPLEX  such that
A1: ( y = x + w & x in B & w in A ) ;
 ( B c= REAL & A c= REAL ) by MEMBERED:3;
then reconsider x = x, w = w as Element of REAL by A1;
take x = x; ::_thesis: ex w being Element of REAL st
( x in B & w in A & y = x + w )
take w = w; ::_thesis: ( x in B & w in A & y = x + w )
thus  ( x in B & w in A & y = x + w ) by A1; ::_thesis: verum
end;
given w, z being Real such that A2: ( w in B & z in A & y = w + z ) ; ::_thesis: y in B ++ A
thus  y in B ++ A by A2, MEMBER_1:46; ::_thesis: verum
end;

theorem :: MEASURE6:22
for A, B being non empty Interval st sup A = inf B & ( sup A in A or inf B in B ) holds
A \/ B is Interval
proof
let A, B be non empty Interval; ::_thesis: ( sup A = inf B & ( sup A in A or inf B in B ) implies A \/ B is Interval )
assume that
A1: sup A = inf B and
A2: ( sup A in A or inf B in B ) ; ::_thesis: A \/ B is Interval
 ( A is right_end or B is left_end ) by A2, XXREAL_2:def_5, XXREAL_2:def_6;
hence  A \/ B is Interval by A1, XXREAL_2:90, XXREAL_2:91; ::_thesis: verum
end;

definition
let A be real-membered set ;
let x be real number ;
:: original: ++
redefine funcx ++ A ->  Subset of REAL;
coherence
 x ++ A is Subset of REAL by MEMBERED:3;
end;

Lm1:  for A being real-membered set
for x being real number
for y being Real holds
( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
proof
let A be real-membered set ; ::_thesis: for x being real number
for y being Real holds
( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
let x be real number ; ::_thesis: for y being Real holds
( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
let y be Real; ::_thesis: ( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
hereby  ::_thesis: ( ex z being Real st
( z in A & y = x + z ) implies y in x ++ A )
assume  y in x ++ A ; ::_thesis: ex w being Element of REAL st
( w in A & y = x + w )
then consider w being Element of COMPLEX  such that
A1: ( y = x + w & w in A ) by MEMBER_1:143;
 A c= REAL by MEMBERED:3;
then reconsider w = w as Element of REAL by A1;
take w = w; ::_thesis: ( w in A & y = x + w )
thus  ( w in A & y = x + w ) by A1; ::_thesis: verum
end;
given z being Real such that A2: ( z in A & y = x + z ) ; ::_thesis: y in x ++ A
thus  y in x ++ A by A2, MEMBER_1:141; ::_thesis: verum
end;

theorem Th23: :: MEASURE6:23
for A being Subset of REAL
for x being real number holds (- x) ++ (x ++ A) = A
proof
let A be Subset of REAL; ::_thesis: for x being real number holds (- x) ++ (x ++ A) = A
let x be real number ; ::_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 A1: y in (- x) ++ (x ++ A) ; ::_thesis: y in A
then reconsider y = y as Real ;
consider z being Real such that
A2: z in x ++ A and
A3: y = (- x) + z by A1, Lm1;
 ex t being Real st
( t in A & z = x + t ) by A2, Lm1;
hence  y in A by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in (- x) ++ (x ++ A) )
assume A4: y in A ; ::_thesis: y in (- x) ++ (x ++ A)
then reconsider y = y as real number ;
reconsider t = y - (- x) as Real by XREAL_0:def_1;
reconsider z = t - x as Real ;
A5: z = (- x) + t ;
 t in x ++ A by A4, Lm1;
hence  y in (- x) ++ (x ++ A) by A5, Lm1; ::_thesis: verum
end;

theorem :: MEASURE6:24
for x being real number
for A being Subset of REAL st A = REAL holds
x ++ A = A
proof
let x be real number ; ::_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 A1: A = REAL ; ::_thesis: x ++ A = A
 A c= x ++ A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or 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 ;
hence  y in x ++ A by A1, Lm1; ::_thesis: verum
end;
hence  x ++ A = A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: MEASURE6:25
for x being real number holds x ++ {} = {} ;

theorem Th26: :: MEASURE6:26
for A being Interval
for x being real number holds
( A is open_interval iff x ++ A is open_interval )
proof
let A be Interval; ::_thesis: for x being real number holds
( A is open_interval iff x ++ A is open_interval )
let x be real number ; ::_thesis: ( A is open_interval iff x ++ A is open_interval )
reconsider y = - x as Real by XREAL_0:def_1;
A1: for B being Interval
for y being real number st B is open_interval holds
y ++ B is open_interval
proof
let B be Interval; ::_thesis: for y being real number st B is open_interval holds
y ++ B is open_interval
let y be real number ; ::_thesis: ( B is open_interval implies y ++ B is open_interval )
reconsider y = y as Real by XREAL_0:def_1;
reconsider z = y as R_eal by XXREAL_0:def_1;
assume  B is open_interval ; ::_thesis: y ++ B is open_interval
then consider a, b being R_eal such that
A2: B = ].a,b.[ by MEASURE5:def_2;
reconsider s = z + a, t = z + b as R_eal ;
 y ++ B = ].s,t.[
proof
thus  y ++ B c= ].s,t.[ :: according to XBOOLE_0:def_10 ::_thesis: ].s,t.[ c= y ++ B
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in ].s,t.[ )
assume A3: c in y ++ B ; ::_thesis: c in ].s,t.[
then reconsider c = c as Real ;
consider d being Real such that
A4: d in B and
A5: c = y + d by A3, Lm1;
reconsider d1 = d as R_eal by XXREAL_0:def_1;
 a < d1 by A2, A4, MEASURE5:def_1;
then A6: s < z + d1 by XXREAL_3:43;
 d1 < b by A2, A4, MEASURE5:def_1;
then A7: z + d1 < t by XXREAL_3:43;
 z + d1 = c by A5, SUPINF_2:1;
hence  c in ].s,t.[ by A6, A7; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in ].s,t.[ or c in y ++ B )
assume A8: c in ].s,t.[ ; ::_thesis: c in y ++ B
then reconsider c = c as Real ;
reconsider c1 = c as R_eal by XXREAL_0:def_1;
A9: c = y + (c - y) ;
 c1 < z + b by A8, MEASURE5:def_1;
then  c1 - z < (b + z) - z by XXREAL_3:43;
then A10: c1 - z < b by XXREAL_3:22;
 z + a < c1 by A8, MEASURE5:def_1;
then  (a + z) - z < c1 - z by XXREAL_3:43;
then A11: a < c1 - z by XXREAL_3:22;
 c1 - z = c - y by SUPINF_2:3;
then  c - y in B by A2, A11, A10;
hence  c in y ++ B by A9, Lm1; ::_thesis: verum
end;
hence  y ++ B is open_interval by MEASURE5:def_2; ::_thesis: verum
end;
hence  ( A is open_interval implies x ++ A is open_interval ) ; ::_thesis: ( x ++ A is open_interval implies A is open_interval )
assume A12: x ++ A is open_interval ; ::_thesis: A is open_interval
then reconsider B = x ++ A as Interval ;
 y ++ B = A by Th23;
hence  A is open_interval by A1, A12; ::_thesis: verum
end;

theorem Th27: :: MEASURE6:27
for A being Interval
for x being real number holds
( A is closed_interval iff x ++ A is closed_interval )
proof
let A be Interval; ::_thesis: for x being real number holds
( A is closed_interval iff x ++ A is closed_interval )
let x be real number ; ::_thesis: ( A is closed_interval iff x ++ A is closed_interval )
A1: for B being Interval
for y being real number st B is closed_interval holds
y ++ B is closed_interval
proof
let B be Interval; ::_thesis: for y being real number st B is closed_interval holds
y ++ B is closed_interval
let y be real number ; ::_thesis: ( B is closed_interval implies y ++ B is closed_interval )
reconsider y = y as Real by XREAL_0:def_1;
reconsider z = y as R_eal by XXREAL_0:def_1;
assume  B is closed_interval ; ::_thesis: y ++ B is closed_interval
then consider a1, b1 being real number  such that
A2: B = [.a1,b1.] by MEASURE5:def_3;
reconsider a = a1, b = b1 as R_eal by XXREAL_0:def_1;
reconsider s = z + a, t = z + b as R_eal ;
 y ++ B = [.s,t.]
proof
thus  y ++ B c= [.s,t.] :: according to XBOOLE_0:def_10 ::_thesis: [.s,t.] c= y ++ B
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in [.s,t.] )
assume A3: c in y ++ B ; ::_thesis: c in [.s,t.]
then reconsider c = c as Real ;
consider d being Real such that
A4: d in B and
A5: c = y + d by A3, Lm1;
reconsider d1 = d as R_eal by XXREAL_0:def_1;
 a <= d1 by A2, A4, XXREAL_1:1;
then A6: s <= z + d1 by XXREAL_3:36;
 d1 <= b by A2, A4, XXREAL_1:1;
then A7: z + d1 <= t by XXREAL_3:36;
 z + d1 = c by A5, SUPINF_2:1;
hence  c in [.s,t.] by A6, A7, XXREAL_1:1; ::_thesis: verum
end;
reconsider a = a, b = b as R_eal ;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in [.s,t.] or c in y ++ B )
assume A8: c in [.s,t.] ; ::_thesis: c in y ++ B
then reconsider c = c as Real by XREAL_0:def_1;
reconsider c1 = c as R_eal by XXREAL_0:def_1;
A9: c = y + (c - y) ;
 c1 <= z + b by A8, XXREAL_1:1;
then  c1 - z <= (b + z) - z by XXREAL_3:36;
then A10: c1 - z <= b by XXREAL_3:22;
 z + a <= c1 by A8, XXREAL_1:1;
then  (a + z) - z <= c1 - z by XXREAL_3:36;
then A11: a <= c1 - z by XXREAL_3:22;
 c1 - z = c - y by SUPINF_2:3;
then  c - y in B by A2, A11, A10;
hence  c in y ++ B by A9, Lm1; ::_thesis: verum
end;
hence  y ++ B is closed_interval by MEASURE5:def_3; ::_thesis: verum
end;
 ( x ++ A is closed_interval implies A is closed_interval )
proof
reconsider y = - x as Real by XREAL_0:def_1;
assume A12: x ++ A is closed_interval ; ::_thesis: A is closed_interval
then reconsider B = x ++ A as Interval ;
 y ++ B = A by Th23;
hence  A is closed_interval by A1, A12; ::_thesis: verum
end;
hence  ( A is closed_interval iff x ++ A is closed_interval ) by A1; ::_thesis: verum
end;

theorem Th28: :: MEASURE6:28
for A being Interval
for x being real number holds
( A is right_open_interval iff x ++ A is right_open_interval )
proof
let A be Interval; ::_thesis: for x being real number holds
( A is right_open_interval iff x ++ A is right_open_interval )
let x be real number ; ::_thesis: ( A is right_open_interval iff x ++ A is right_open_interval )
A1: for B being Interval
for y being real number st B is right_open_interval holds
y ++ B is right_open_interval
proof
let B be Interval; ::_thesis: for y being real number st B is right_open_interval holds
y ++ B is right_open_interval
let y be real number ; ::_thesis: ( B is right_open_interval implies y ++ B is right_open_interval )
reconsider y = y as Real by XREAL_0:def_1;
reconsider z = y as R_eal by XXREAL_0:def_1;
assume  B is right_open_interval ; ::_thesis: y ++ B is right_open_interval
then consider a1 being real number , b being R_eal such that
A2: B = [.a1,b.[ by MEASURE5:def_4;
reconsider a = a1 as R_eal by XXREAL_0:def_1;
reconsider s = z + a, t = z + b as R_eal ;
 y ++ B = [.s,t.[
proof
thus  y ++ B c= [.s,t.[ :: according to XBOOLE_0:def_10 ::_thesis: [.s,t.[ c= y ++ B
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in [.s,t.[ )
assume A3: c in y ++ B ; ::_thesis: c in [.s,t.[
then reconsider c = c as Real ;
consider d being Real such that
A4: d in B and
A5: c = y + d by A3, Lm1;
reconsider d1 = d as R_eal by XXREAL_0:def_1;
 a <= d1 by A2, A4, XXREAL_1:3;
then A6: s <= z + d1 by XXREAL_3:36;
 d1 < b by A2, A4, XXREAL_1:3;
then A7: z + d1 < t by XXREAL_3:43;
 z + d1 = c by A5, SUPINF_2:1;
hence  c in [.s,t.[ by A6, A7, XXREAL_1:3; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in [.s,t.[ or c in y ++ B )
assume A8: c in [.s,t.[ ; ::_thesis: c in y ++ B
then reconsider c = c as Real by XREAL_0:def_1;
reconsider c1 = c as R_eal by XXREAL_0:def_1;
A9: c = y + (c - y) ;
 c1 < z + b by A8, XXREAL_1:3;
then  c1 - z < (b + z) - z by XXREAL_3:43;
then A10: c1 - z < b by XXREAL_3:22;
 z + a <= c1 by A8, XXREAL_1:3;
then  (a + z) - z <= c1 - z by XXREAL_3:36;
then A11: a <= c1 - z by XXREAL_3:22;
 c1 - z = c - y by SUPINF_2:3;
then  c - y in B by A2, A11, A10;
hence  c in y ++ B by A9, Lm1; ::_thesis: verum
end;
hence  y ++ B is right_open_interval by MEASURE5:def_4; ::_thesis: verum
end;
 ( x ++ A is right_open_interval implies A is right_open_interval )
proof
reconsider y = - x as Real by XREAL_0:def_1;
assume A12: x ++ A is right_open_interval ; ::_thesis: A is right_open_interval
then reconsider B = x ++ A as Interval ;
 y ++ B = A by Th23;
hence  A is right_open_interval by A1, A12; ::_thesis: verum
end;
hence  ( A is right_open_interval iff x ++ A is right_open_interval ) by A1; ::_thesis: verum
end;

theorem Th29: :: MEASURE6:29
for A being Interval
for x being real number holds
( A is left_open_interval iff x ++ A is left_open_interval )
proof
let A be Interval; ::_thesis: for x being real number holds
( A is left_open_interval iff x ++ A is left_open_interval )
let x be real number ; ::_thesis: ( A is left_open_interval iff x ++ A is left_open_interval )
A1: for B being Interval
for y being real number st B is left_open_interval holds
y ++ B is left_open_interval
proof
let B be Interval; ::_thesis: for y being real number st B is left_open_interval holds
y ++ B is left_open_interval
let y be real number ; ::_thesis: ( B is left_open_interval implies y ++ B is left_open_interval )
reconsider y = y as Real by XREAL_0:def_1;
reconsider z = y as R_eal by XXREAL_0:def_1;
assume  B is left_open_interval ; ::_thesis: y ++ B is left_open_interval
then consider a being R_eal, b1 being real number  such that
A2: B = ].a,b1.] by MEASURE5:def_5;
reconsider b = b1 as R_eal by XXREAL_0:def_1;
set s = z + a;
set t = z + b;
 y ++ B = ].(z + a),(z + b).]
proof
thus  y ++ B c= ].(z + a),(z + b).] :: according to XBOOLE_0:def_10 ::_thesis: ].(z + a),(z + b).] c= y ++ B
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in ].(z + a),(z + b).] )
assume A3: c in y ++ B ; ::_thesis: c in ].(z + a),(z + b).]
then reconsider c = c as Real ;
consider d being Real such that
A4: d in B and
A5: c = y + d by A3, Lm1;
reconsider d1 = d as R_eal by XXREAL_0:def_1;
 a < d1 by A2, A4, XXREAL_1:2;
then A6: z + a < z + d1 by XXREAL_3:43;
 d1 <= b by A2, A4, XXREAL_1:2;
then A7: z + d1 <= z + b by XXREAL_3:36;
 z + d1 = c by A5, SUPINF_2:1;
hence  c in ].(z + a),(z + b).] by A6, A7, XXREAL_1:2; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in ].(z + a),(z + b).] or c in y ++ B )
assume A8: c in ].(z + a),(z + b).] ; ::_thesis: c in y ++ B
then reconsider c = c as Real by XREAL_0:def_1;
reconsider c1 = c as R_eal by XXREAL_0:def_1;
A9: c = y + (c - y) ;
 c1 <= z + b by A8, XXREAL_1:2;
then  c1 - z <= (b + z) - z by XXREAL_3:36;
then A10: c1 - z <= b by XXREAL_3:22;
 z + a < c1 by A8, XXREAL_1:2;
then  (a + z) - z < c1 - z by XXREAL_3:43;
then A11: a < c1 - z by XXREAL_3:22;
 c1 - z = c - y by SUPINF_2:3;
then  c - y in B by A2, A11, A10;
hence  c in y ++ B by A9, Lm1; ::_thesis: verum
end;
hence  y ++ B is left_open_interval by MEASURE5:def_5; ::_thesis: verum
end;
 ( x ++ A is left_open_interval implies A is left_open_interval )
proof
reconsider y = - x as Real by XREAL_0:def_1;
assume A12: x ++ A is left_open_interval ; ::_thesis: A is left_open_interval
then reconsider B = x ++ A as Interval ;
 y ++ B = A by Th23;
hence  A is left_open_interval by A1, A12; ::_thesis: verum
end;
hence  ( A is left_open_interval iff x ++ A is left_open_interval ) by A1; ::_thesis: verum
end;

theorem :: MEASURE6:30
for A being Interval
for x being real number holds x ++ A is Interval
proof
let A be Interval; ::_thesis: for x being real number holds x ++ A is Interval
let x be real number ; ::_thesis: 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;
suppose A is open_interval ; ::_thesis: x ++ A is Interval
then  x ++ A is open_interval by Th26;
hence  x ++ A is Interval ; ::_thesis: verum
end;
suppose A is closed_interval ; ::_thesis: x ++ A is Interval
then  x ++ A is closed_interval by Th27;
hence  x ++ A is Interval ; ::_thesis: verum
end;
suppose A is right_open_interval ; ::_thesis: x ++ A is Interval
then  x ++ A is right_open_interval by Th28;
hence  x ++ A is Interval ; ::_thesis: verum
end;
suppose A is left_open_interval ; ::_thesis: x ++ A is Interval
then  x ++ A is left_open_interval by Th29;
hence  x ++ A is Interval ; ::_thesis: verum
end;
end;
end;

theorem Th31: :: MEASURE6:31
for A being real-membered set
for x being real number
for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)
proof
let A be real-membered set ; ::_thesis: for x being real number
for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)
let x be real number ; ::_thesis: for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)
let y be R_eal; ::_thesis: ( x = y implies sup (x ++ A) = y + (sup A) )
assume A1: x = y ; ::_thesis: sup (x ++ A) = y + (sup A)
A2: for z being UpperBound of x ++ A holds y + (sup A) <= z
proof
let z be UpperBound of x ++ A; ::_thesis: y + (sup A) <= z
reconsider zz = z as R_eal by XXREAL_0:def_1;
 zz - y is UpperBound of A
proof
let u be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not u in A or u <= zz - y )
reconsider uu = u as R_eal by XXREAL_0:def_1;
assume A3: u in A ; ::_thesis: u <= zz - y
then reconsider u1 = u as Real by XREAL_0:def_1;
 y + uu = x + u1 by A1, XXREAL_3:def_2;
then  y + uu in x ++ A by A3, Lm1;
then  y + uu <= z by XXREAL_2:def_1;
hence  u <= zz - y by A1, XXREAL_3:45; ::_thesis: verum
end;
then  sup A <= zz - y by XXREAL_2:def_3;
hence  y + (sup A) <= z by A1, XXREAL_3:45; ::_thesis: verum
end;
 y + (sup A) is UpperBound of x ++ A
proof
let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not z in x ++ A or z <= y + (sup A) )
assume  z in x ++ A ; ::_thesis: z <= y + (sup A)
then consider a being Real such that
A4: a in A and
A5: z = x + a by Lm1;
reconsider b = a as R_eal by XXREAL_0:def_1;
A6: a <= sup A by A4, XXREAL_2:4;
 ex a, c being complex number st
( y = a & b = c & y + b = a + c ) by A1, XXREAL_3:def_2;
hence  z <= y + (sup A) by A1, A5, A6, XXREAL_3:36; ::_thesis: verum
end;
hence  sup (x ++ A) = y + (sup A) by A2, XXREAL_2:def_3; ::_thesis: verum
end;

theorem Th32: :: MEASURE6:32
for A being real-membered set
for x being real number
for y being R_eal st x = y holds
inf (x ++ A) = y + (inf A)
proof
let A be real-membered set ; ::_thesis: for x being real number
for y being R_eal st x = y holds
inf (x ++ A) = y + (inf A)
let x be real number ; ::_thesis: for y being R_eal st x = y holds
inf (x ++ A) = y + (inf A)
let y be R_eal; ::_thesis: ( x = y implies inf (x ++ A) = y + (inf A) )
assume A1: x = y ; ::_thesis: inf (x ++ A) = y + (inf A)
A2: for z being LowerBound of x ++ A holds z <= y + (inf A)
proof
let z be LowerBound of x ++ A; ::_thesis: z <= y + (inf A)
reconsider zz = z as R_eal by XXREAL_0:def_1;
 zz - y is LowerBound of A
proof
let u be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not u in A or zz - y <= u )
reconsider uu = u as R_eal by XXREAL_0:def_1;
assume A3: u in A ; ::_thesis: zz - y <= u
then reconsider u1 = u as Real by XREAL_0:def_1;
 y + uu = x + u1 by A1, XXREAL_3:def_2;
then  y + uu in x ++ A by A3, Lm1;
then  z <= y + uu by XXREAL_2:def_2;
hence  zz - y <= u by A1, XXREAL_3:42; ::_thesis: verum
end;
then  zz - y <= inf A by XXREAL_2:def_4;
hence  z <= y + (inf A) by A1, XXREAL_3:41; ::_thesis: verum
end;
 y + (inf A) is LowerBound of x ++ A
proof
let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not z in x ++ A or y + (inf A) <= z )
assume  z in x ++ A ; ::_thesis: y + (inf A) <= z
then consider a being Real such that
A4: a in A and
A5: z = x + a by Lm1;
reconsider b = a as R_eal by XXREAL_0:def_1;
A6: inf A <= a by A4, XXREAL_2:3;
 ex a, c being complex number st
( y = a & b = c & y + b = a + c ) by A1, XXREAL_3:def_2;
hence  y + (inf A) <= z by A1, A5, A6, XXREAL_3:36; ::_thesis: verum
end;
hence  inf (x ++ A) = y + (inf A) by A2, XXREAL_2:def_4; ::_thesis: verum
end;

theorem :: MEASURE6:33
for A being Interval
for x being real number holds diameter A = diameter (x ++ A)
proof
let A be Interval; ::_thesis: for x being real number holds diameter A = diameter (x ++ A)
let x be real number ; ::_thesis: diameter A = diameter (x ++ A)
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: diameter A = diameter (x ++ A)
hence  diameter A = diameter (x ++ A) ; ::_thesis: verum
end;
supposeA1: not A is empty ; ::_thesis: diameter A = diameter (x ++ A)
then consider y being real number  such that
A2: y in A by MEMBERED:9;
reconsider y = y as Real by XREAL_0:def_1;
A3: x + y in x ++ A by A2, Lm1;
reconsider y = x as R_eal by XXREAL_0:def_1;
thus  diameter A = (sup A) - (inf A) by A1, MEASURE5:def_6
.= (y + (sup A)) - (y + (inf A)) by XXREAL_3:33
.= (sup (x ++ A)) - (y + (inf A)) by Th31
.= (sup (x ++ A)) - (inf (x ++ A)) by Th32
.= diameter (x ++ A) by A3, MEASURE5:def_6 ; ::_thesis: verum
end;
end;
end;

begin

notation
let X be set ;
synonym  without_zero X for  with_non-empty_elements ;
antonym  with_zero X for  with_non-empty_elements ;
end;

definition
let X be set ;
redefine attr X is with_non-empty_elements  means :Def2: :: MEASURE6:def 2
 not 0 in X;
compatibility
 ( X is without_zero iff not 0 in X ) by SETFAM_1:def_8;
end;

:: deftheorem Def2 defines without_zero MEASURE6:def_2_:_
 for X being set holds
( X is without_zero iff not 0 in X );

registration
cluster REAL  ->  with_zero ;
coherence
 not REAL is without_zero by Def2;
cluster omega  ->  with_zero ;
coherence
 not NAT is without_zero by Def2;
end;

registration
cluster non empty without_zero for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is without_zero )
proof
set s = {1};
take  {1} ; ::_thesis: ( not {1} is empty & {1} is without_zero )
thus  not {1} is empty ; ::_thesis: {1} is without_zero
thus  {1} is without_zero ; ::_thesis: verum
end;
cluster non empty with_zero for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is with_zero ) by Def2;
end;

registration
cluster non empty complex-membered ext-real-membered real-membered without_zero for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty & b1 is without_zero )
proof
set s = {1};
take  {1} ; ::_thesis: ( not {1} is empty & {1} is without_zero )
thus  not {1} is empty ; ::_thesis: {1} is without_zero
thus  {1} is without_zero ; ::_thesis: verum
end;
cluster non empty complex-membered ext-real-membered real-membered with_zero for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty & b1 is with_zero ) by Def2;
end;

theorem Th34: :: MEASURE6:34
for F being set st not F is empty & F is with_non-empty_elements & F is c=-linear holds
F is centered
proof
defpred S1[ set ] means ( $1 <> {} implies ex x being set st
( x in $1 & ( for y being set st y in $1 holds
x c= y ) ) );
let F be set ; ::_thesis: ( not F is empty & F is with_non-empty_elements & F is c=-linear implies F is centered )
assume that
A1: not F is empty and
A2: F is with_non-empty_elements and
A3: F is c=-linear ; ::_thesis: F is centered
thus  F <> {} by A1; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds
( b1 = {} or not b1 c= F or not b1 is finite or not meet b1 = {} )
let G be set ; ::_thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} )
assume that
A4: G <> {} and
A5: G c= F and
A6: G is finite ; ::_thesis: not meet G = {}
A7: now__::_thesis:_for_x,_B_being_set_st_x_in_G_&_B_c=_G_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in G & B c= G & S1[B] implies S1[B \/ {x}] )
assume that
A8: x in G and
A9: B c= G and
A10: S1[B] ; ::_thesis: S1[B \/ {x}]
thus  S1[B \/ {x}] ::_thesis: verum
proof
assume  B \/ {x} <> {} ; ::_thesis: ex x being set st
( x in B \/ {x} & ( for y being set st y in B \/ {x} holds
x c= y ) )
percases ( B is empty or not B is empty ) ;
supposeA11: B is empty ; ::_thesis: ex x being set st
( x in B \/ {x} & ( for y being set st y in B \/ {x} holds
x c= y ) )
take x9 = x; ::_thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
thus  x9 in B \/ {x} by A11, TARSKI:def_1; ::_thesis: for y being set st y in B \/ {x} holds
x9 c= y
let y be set ; ::_thesis: ( y in B \/ {x} implies x9 c= y )
thus  ( y in B \/ {x} implies x9 c= y ) by A11, TARSKI:def_1; ::_thesis: verum
end;
suppose not B is empty ; ::_thesis: ex x being set st
( x in B \/ {x} & ( for y being set st y in B \/ {x} holds
x c= y ) )
then consider z being set  such that
A12: z in B and
A13: for y being set st y in B holds
z c= y by A10;
thus  ex x9 being set st
( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) ) ::_thesis: verum
proof
 z in G by A9, A12;
then A14: x,z are_c=-comparable by A3, A5, A8, ORDINAL1:def_8;
percases ( x c= z or z c= x ) by A14, XBOOLE_0:def_9;
supposeA15: x c= z ; ::_thesis: ex x9 being set st
( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
take x9 = x; ::_thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
 x9 in {x} by TARSKI:def_1;
hence  x9 in B \/ {x} by XBOOLE_0:def_3; ::_thesis: for y being set st y in B \/ {x} holds
x9 c= y
let y be set ; ::_thesis: ( y in B \/ {x} implies x9 c= y )
assume A16: y in B \/ {x} ; ::_thesis: x9 c= y
percases ( y in B or y in {x} ) by A16, XBOOLE_0:def_3;
suppose y in B ; ::_thesis: x9 c= y
then  z c= y by A13;
hence  x9 c= y by A15, XBOOLE_1:1; ::_thesis: verum
end;
suppose y in {x} ; ::_thesis: x9 c= y
hence  x9 c= y by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
supposeA17: z c= x ; ::_thesis: ex x9 being set st
( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
take x9 = z; ::_thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds
x9 c= y ) )
thus  x9 in B \/ {x} by A12, XBOOLE_0:def_3; ::_thesis: for y being set st y in B \/ {x} holds
x9 c= y
let y be set ; ::_thesis: ( y in B \/ {x} implies x9 c= y )
assume A18: y in B \/ {x} ; ::_thesis: x9 c= y
percases ( y in B or y in {x} ) by A18, XBOOLE_0:def_3;
suppose y in B ; ::_thesis: x9 c= y
hence  x9 c= y by A13; ::_thesis: verum
end;
suppose y in {x} ; ::_thesis: x9 c= y
hence  x9 c= y by A17, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
A19: S1[ {} ] ;
 S1[G] from FINSET_1:sch_2(A6, A19, A7);
then consider x being set  such that
A20: x in G and
A21: for y being set st y in G holds
x c= y by A4;
consider xe being set  such that
A22: xe in x by A2, A5, A20, XBOOLE_0:def_1;
now__::_thesis:_for_y_being_set_st_y_in_G_holds_
xe_in_y
let y be set ; ::_thesis: ( y in G implies xe in y )
assume  y in G ; ::_thesis: xe in y
then  x c= y by A21;
hence  xe in y by A22; ::_thesis: verum
end;
hence  not meet G = {} by A4, SETFAM_1:def_1; ::_thesis: verum
end;

registration
let F be set ;
cluster c=-linear non empty with_non-empty_elements  ->  centered for Element of bool (bool F);
coherence
 for b1 being Subset-Family of F st not b1 is empty & b1 is with_non-empty_elements & b1 is c=-linear holds
b1 is centered by Th34;
end;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
clusterf .: X ->  non empty ;
coherence
 not f .: X is empty
proof
set x = the Element of X;
A1: dom f = X by FUNCT_2:def_1;
thus  not f .: X is empty by A1; ::_thesis: verum
end;
end;

definition
let X, Y be set ;
let f be Function of X,Y;
func " f ->  Function of (bool Y),(bool X) means :Def3: :: MEASURE6:def 3
 for y being Subset of Y holds it . y = f " y;
existence
 ex b1 being Function of (bool Y),(bool X) st
for y being Subset of Y holds b1 . y = f " y
proof
deffunc H1( Subset of Y) ->  Element of bool X = f " $1;
thus  ex T being Function of (bool Y),(bool X) st
for y being Subset of Y holds T . y = H1(y) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (bool Y),(bool X) st ( for y being Subset of Y holds b1 . y = f " y ) & ( for y being Subset of Y holds b2 . y = f " y ) holds
b1 = b2
proof
deffunc H1( Subset of Y) ->  Element of bool X = f " $1;
thus  for T1, T2 being Function of (bool Y),(bool X) st ( for y being Subset of Y holds T1 . y = H1(y) ) & ( for y being Subset of Y holds T2 . y = H1(y) ) holds
T1 = T2 from BINOP_2:sch_1(); ::_thesis: verum
end;
end;

:: deftheorem Def3 defines " MEASURE6:def_3_:_
 for X, Y being set
for f being Function of X,Y
for b4 being Function of (bool Y),(bool X) holds
( b4 = " f iff for y being Subset of Y holds b4 . y = f " y );

theorem :: MEASURE6:35
for X, Y, x being set
for S being Subset-Family of Y
for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S
proof
let X, Y, x be set ; ::_thesis: for S being Subset-Family of Y
for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S
let S be Subset-Family of Y; ::_thesis: for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S
let f be Function of X,Y; ::_thesis: ( x in meet ((" f) .: S) implies f . x in meet S )
assume A1: x in meet ((" f) .: S) ; ::_thesis: f . x in meet S
A2: now__::_thesis:_for_SS_being_set_st_SS_in_S_holds_
f_._x_in_SS
let SS be set ; ::_thesis: ( SS in S implies f . x in SS )
assume A3: SS in S ; ::_thesis: f . x in SS
then  (" f) . SS in (" f) .: S by FUNCT_2:35;
then A4: x in (" f) . SS by A1, SETFAM_1:def_1;
 (" f) . SS = f " SS by A3, Def3;
hence  f . x in SS by A4, FUNCT_1:def_7; ::_thesis: verum
end;
 not (" f) .: S is empty by A1, SETFAM_1:def_1;
then  not S is empty ;
hence  f . x in meet S by A2, SETFAM_1:def_1; ::_thesis: verum
end;


theorem Th36: :: MEASURE6:36
for r, s being real number st (abs r) + (abs s) = 0 holds
r = 0
proof
let r, s be real number ; ::_thesis: ( (abs r) + (abs s) = 0 implies r = 0 )
set aa = abs r;
set ab = abs s;
A1: ( 0 <= abs r & 0 <= abs s ) by COMPLEX1:46;
assume  (abs r) + (abs s) = 0 ; ::_thesis: r = 0
then  abs r = 0 by A1;
hence  r = 0 by ABSVALUE:2; ::_thesis: verum
end;

theorem Th37: :: MEASURE6:37
for r, s, t being real number st r < s & s < t holds
abs s < (abs r) + (abs t)
proof
let r, s, t be real number ; ::_thesis: ( r < s & s < t implies abs s < (abs r) + (abs t) )
assume that
A1: r < s and
A2: s < t ; ::_thesis: abs s < (abs r) + (abs t)
percases ( s < 0 or 0 <= s ) ;
supposeA3: s < 0 ; ::_thesis: abs s < (abs r) + (abs t)
 - s < - r by A1, XREAL_1:24;
then A4: (- s) + 0 < (- r) + (abs t) by COMPLEX1:46, XREAL_1:8;
 - s = abs s by A3, ABSVALUE:def_1;
hence  abs s < (abs r) + (abs t) by A1, A3, A4, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA5: 0 <= s ; ::_thesis: abs s < (abs r) + (abs t)
A6: s + 0 < t + (abs r) by A2, COMPLEX1:46, XREAL_1:8;
 s = abs s by A5, ABSVALUE:def_1;
hence  abs s < (abs r) + (abs t) by A2, A5, A6, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;


theorem Th38: :: MEASURE6:38
for seq being Real_Sequence st seq is convergent & seq is non-zero & lim seq = 0 holds
not seq " is bounded
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & seq is non-zero & lim seq = 0 implies not seq " is bounded )
assume that
A1: seq is convergent and
A2: seq is non-zero and
A3: lim seq = 0 ; ::_thesis: not seq " is bounded
given r being real number  such that A4: for n being Element of NAT holds (seq ") . n < r ; :: according to SEQ_2:def_3,SEQ_2:def_8 ::_thesis: not seq " is bounded_below
given s being real number  such that A5: for n being Element of NAT holds s < (seq ") . n ; :: according to SEQ_2:def_4 ::_thesis: contradiction
set aa = abs r;
set ab = abs s;
set rab = 1 / ((abs r) + (abs s));
A6: ( 0 <= abs r & 0 <= abs s ) by COMPLEX1:46;
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_(seq_._n)_>_1_/_((abs_r)_+_(abs_s))
let n be Element of NAT ; ::_thesis: abs (seq . n) > 1 / ((abs r) + (abs s))
set g = seq . n;
set t = (seq ") . n;
set At = abs ((seq ") . n);
 (seq ") . n = 1 / (seq . n) by VALUED_1:10;
then A8: abs ((seq ") . n) = 1 / (abs (seq . n)) by ABSVALUE:7;
 ((seq ") . n) " = ((seq . n) ") " by VALUED_1:10;
then  (seq ") . n <> 0 by A2, SEQ_1:5, XCMPLX_1:202;
then A9: 0 < abs ((seq ") . n) by COMPLEX1:47;
 ( s < (seq ") . n & (seq ") . n < r ) by A4, A5;
then  abs ((seq ") . n) < (abs r) + (abs s) by Th37;
then  (abs ((seq ") . n)) " > ((abs r) + (abs s)) " by A9, XREAL_1:88;
hence  abs (seq . n) > 1 / ((abs r) + (abs s)) by A8; ::_thesis: verum
end;
A10: (seq ") . 1 < r by A4;
A11: s < (seq ") . 1 by A5;
now__::_thesis:_not_0_>=_(abs_r)_+_(abs_s)
assume  0 >= (abs r) + (abs s) ; ::_thesis: contradiction
then A12: (abs r) + (abs s) = 0 by A6;
then  r = 0 by Th36;
hence  contradiction by A11, A10, A12, Th36; ::_thesis: verum
end;
then consider n being Element of NAT  such that
A13: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < 1 / ((abs r) + (abs s)) by A1, A3, SEQ_2:def_7;
 abs ((seq . n) - 0) < 1 / ((abs r) + (abs s)) by A13;
hence  contradiction by A7; ::_thesis: verum
end;

theorem Th39: :: MEASURE6:39
for seq being Real_Sequence holds
( rng seq is real-bounded iff seq is bounded )
proof
let seq be Real_Sequence; ::_thesis: ( rng seq is real-bounded iff seq is bounded )
thus  ( rng seq is real-bounded implies seq is bounded ) ::_thesis: ( seq is bounded implies rng seq is real-bounded )
proof
given s being real number  such that A1: s is LowerBound of rng seq ; :: according to XXREAL_2:def_9,XXREAL_2:def_11 ::_thesis: ( not rng seq is bounded_above or seq is bounded )
given t being real number  such that A2: t is UpperBound of rng seq ; :: according to XXREAL_2:def_10 ::_thesis: seq is bounded
thus  seq is bounded_above :: according to SEQ_2:def_8 ::_thesis: seq is bounded_below
proof
take  t + 1 ; :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not t + 1 <= seq . b1
let n be Element of NAT ; ::_thesis: not t + 1 <= seq . n
 ( seq . n <= t & t < t + 1 ) by A2, FUNCT_2:4, XREAL_1:29, XXREAL_2:def_1;
hence  not t + 1 <= seq . n by XXREAL_0:2; ::_thesis: verum
end;
take  s - 1 ; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not seq . b1 <= s - 1
let n be Element of NAT ; ::_thesis: not seq . n <= s - 1
 s < s + 1 by XREAL_1:29;
then A3: s - 1 < s by XREAL_1:19;
 seq . n >= s by A1, FUNCT_2:4, XXREAL_2:def_2;
hence  not seq . n <= s - 1 by A3, XXREAL_0:2; ::_thesis: verum
end;
given t being real number  such that A4: for n being Element of NAT holds seq . n < t ; :: according to SEQ_2:def_3,SEQ_2:def_8 ::_thesis: ( not seq is bounded_below or rng seq is real-bounded )
given s being real number  such that A5: for n being Element of NAT holds seq . n > s ; :: according to SEQ_2:def_4 ::_thesis: rng seq is real-bounded
thus  rng seq is bounded_below :: according to XXREAL_2:def_11 ::_thesis: rng seq is bounded_above
proof
take  s ; :: according to XXREAL_2:def_9 ::_thesis: s is LowerBound of rng seq
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in rng seq or s <= r )
assume  r in rng seq ; ::_thesis: s <= r
then  ex n being set st
( n in dom seq & seq . n = r ) by FUNCT_1:def_3;
hence  s <= r by A5; ::_thesis: verum
end;
take  t ; :: according to XXREAL_2:def_10 ::_thesis: t is UpperBound of rng seq
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in rng seq or r <= t )
assume  r in rng seq ; ::_thesis: r <= t
then  ex n being set st
( n in dom seq & seq . n = r ) by FUNCT_1:def_3;
hence  r <= t by A4; ::_thesis: verum
end;

notation
let X be real-membered set ;
synonym  with_max X for  right_end ;
synonym  with_min X for  left_end ;
end;

definition
let X be real-membered set ;
redefine attr X is right_end  means :: MEASURE6:def 4
( X is bounded_above & upper_bound X in X );
compatibility
 ( X is with_max iff ( X is bounded_above & upper_bound X in X ) )
proof
thus  ( X is with_max implies ( X is bounded_above & upper_bound X in X ) ) ::_thesis: ( X is bounded_above & upper_bound X in X implies X is with_max )
proof
assume A1: X is with_max ; ::_thesis: ( X is bounded_above & upper_bound X in X )
hence  X is bounded_above ; ::_thesis: upper_bound X in X
reconsider X = X as non empty real-membered bounded_above set by A1;
 upper_bound X in X by A1, XXREAL_2:def_6;
hence  upper_bound X in X ; ::_thesis: verum
end;
assume A2: ( X is bounded_above & upper_bound X in X ) ; ::_thesis: X is with_max
then reconsider X = X as non empty real-membered bounded_above set ;
 upper_bound X in X by A2;
hence  X is with_max by XXREAL_2:def_6; ::_thesis: verum
end;
redefine attr X is left_end  means :: MEASURE6:def 5
( X is bounded_below & lower_bound X in X );
compatibility
 ( X is with_min iff ( X is bounded_below & lower_bound X in X ) )
proof
thus  ( X is with_min implies ( X is bounded_below & lower_bound X in X ) ) ::_thesis: ( X is bounded_below & lower_bound X in X implies X is with_min )
proof
assume A3: X is with_min ; ::_thesis: ( X is bounded_below & lower_bound X in X )
hence  X is bounded_below ; ::_thesis: lower_bound X in X
reconsider X = X as non empty real-membered bounded_below set by A3;
 lower_bound X in X by A3, XXREAL_2:def_5;
hence  lower_bound X in X ; ::_thesis: verum
end;
assume A4: ( X is bounded_below & lower_bound X in X ) ; ::_thesis: X is with_min
then reconsider X = X as non empty real-membered bounded_below set ;
 lower_bound X in X by A4;
hence  X is with_min by XXREAL_2:def_5; ::_thesis: verum
end;
end;

:: deftheorem  defines with_max MEASURE6:def_4_:_
 for X being real-membered set holds
( X is with_max iff ( X is bounded_above & upper_bound X in X ) );

:: deftheorem  defines with_min MEASURE6:def_5_:_
 for X being real-membered set holds
( X is with_min iff ( X is bounded_below & lower_bound X in X ) );

registration
cluster non empty complex-membered ext-real-membered real-membered real-bounded closed for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty & b1 is closed & b1 is real-bounded )
proof
 [.0,0.] = {0} by XXREAL_1:17;
hence  ex b1 being Subset of REAL st
( not b1 is empty & b1 is closed & b1 is real-bounded ) ; ::_thesis: verum
end;
end;

definition
let R be Subset-Family of REAL;
attrR is open  means :: MEASURE6:def 6
 for X being Subset of REAL st X in R holds
X is open ;
attrR is closed  means :Def7: :: MEASURE6:def 7
 for X being Subset of REAL st X in R holds
X is closed ;
end;

:: deftheorem  defines open MEASURE6:def_6_:_
 for R being Subset-Family of REAL holds
( R is open iff for X being Subset of REAL st X in R holds
X is open );

:: deftheorem Def7 defines closed MEASURE6:def_7_:_
 for R being Subset-Family of REAL holds
( R is closed iff for X being Subset of REAL st X in R holds
X is closed );


definition
let X be Subset of REAL;
:: original: --
redefine func -- X ->  Subset of REAL;
coherence
 -- X is Subset of REAL by MEMBERED:3;
end;

theorem :: MEASURE6:40
for r being real number
for X being Subset of REAL holds
( r in X iff - r in -- X ) by MEMBER_1:11;

Lm2:  for X being Subset of REAL st X is bounded_above holds
-- X is bounded_below
proof
let X be Subset of REAL; ::_thesis: ( X is bounded_above implies -- X is bounded_below )
given s being real number  such that A1: s is UpperBound of X ; :: according to XXREAL_2:def_10 ::_thesis: -- X is bounded_below
take  - s ; :: according to XXREAL_2:def_9 ::_thesis: - s is LowerBound of -- X
let t be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not t in -- X or - s <= t )
assume  t in -- X ; ::_thesis: - s <= t
then consider r3 being Element of COMPLEX  such that
A2: t = - r3 and
A3: r3 in X ;
reconsider r3 = r3 as Real by A3;
 r3 <= s by A1, A3, XXREAL_2:def_1;
hence  - s <= t by A2, XREAL_1:24; ::_thesis: verum
end;

Lm3:  for X being Subset of REAL st X is bounded_below holds
-- X is bounded_above
proof
let X be Subset of REAL; ::_thesis: ( X is bounded_below implies -- X is bounded_above )
given s being real number  such that A1: s is LowerBound of X ; :: according to XXREAL_2:def_9 ::_thesis: -- X is bounded_above
take  - s ; :: according to XXREAL_2:def_10 ::_thesis: - s is UpperBound of -- X
let t be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not t in -- X or t <= - s )
assume  t in -- X ; ::_thesis: t <= - s
then consider r3 being Element of COMPLEX  such that
A2: t = - r3 and
A3: r3 in X ;
reconsider r3 = r3 as Real by A3;
 r3 >= s by A1, A3, XXREAL_2:def_2;
hence  t <= - s by A2, XREAL_1:24; ::_thesis: verum
end;

theorem Th41: :: MEASURE6:41
for X being Subset of REAL holds
( X is bounded_above iff -- X is bounded_below )
proof
let X be Subset of REAL; ::_thesis: ( X is bounded_above iff -- X is bounded_below )
 X = -- (-- X) ;
hence  ( X is bounded_above iff -- X is bounded_below ) by Lm2, Lm3; ::_thesis: verum
end;

theorem :: MEASURE6:42
for X being Subset of REAL holds
( X is bounded_below iff -- X is bounded_above )
proof
let X be Subset of REAL; ::_thesis: ( X is bounded_below iff -- X is bounded_above )
 X = -- (-- X) ;
hence  ( X is bounded_below iff -- X is bounded_above ) by Th41; ::_thesis: verum
end;

theorem Th43: :: MEASURE6:43
for X being non empty Subset of REAL st X is bounded_below holds
lower_bound X = - (upper_bound (-- X))
proof
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below implies lower_bound X = - (upper_bound (-- X)) )
set r = - (upper_bound (-- X));
A1: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_X_holds_
s_>=_t_)_holds_
-_(upper_bound_(--_X))_>=_t
let t be real number ; ::_thesis: ( ( for s being real number st s in X holds
s >= t ) implies - (upper_bound (-- X)) >= t )
assume A2: for s being real number st s in X holds
s >= t ; ::_thesis: - (upper_bound (-- X)) >= t
now__::_thesis:_for_s_being_real_number_st_s_in_--_X_holds_
s_<=_-_t
let s be real number ; ::_thesis: ( s in -- X implies s <= - t )
assume  s in -- X ; ::_thesis: s <= - t
then  - s in -- (-- X) by MEMBER_1:11;
then  - s >= t by A2;
then  - (- s) <= - t by XREAL_1:24;
hence  s <= - t ; ::_thesis: verum
end;
then  - (- (upper_bound (-- X))) <= - t by SEQ_4:45;
hence  - (upper_bound (-- X)) >= t by XREAL_1:24; ::_thesis: verum
end;
assume  X is bounded_below ; ::_thesis: lower_bound X = - (upper_bound (-- X))
then A3: -- X is bounded_above by Lm3;
now__::_thesis:_for_s_being_real_number_st_s_in_X_holds_
s_>=_-_(upper_bound_(--_X))
let s be real number ; ::_thesis: ( s in X implies s >= - (upper_bound (-- X)) )
assume  s in X ; ::_thesis: s >= - (upper_bound (-- X))
then  - s in -- X by MEMBER_1:11;
then  - s <= - (- (upper_bound (-- X))) by A3, SEQ_4:def_1;
hence  s >= - (upper_bound (-- X)) by XREAL_1:24; ::_thesis: verum
end;
hence  lower_bound X = - (upper_bound (-- X)) by A1, SEQ_4:44; ::_thesis: verum
end;

theorem Th44: :: MEASURE6:44
for X being non empty Subset of REAL st X is bounded_above holds
upper_bound X = - (lower_bound (-- X))
proof
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above implies upper_bound X = - (lower_bound (-- X)) )
set r = - (lower_bound (-- X));
A1: now__::_thesis:_for_s_being_real_number_st_(_for_t_being_real_number_st_t_in_X_holds_
t_<=_s_)_holds_
-_(lower_bound_(--_X))_<=_s
let s be real number ; ::_thesis: ( ( for t being real number st t in X holds
t <= s ) implies - (lower_bound (-- X)) <= s )
assume A2: for t being real number st t in X holds
t <= s ; ::_thesis: - (lower_bound (-- X)) <= s
now__::_thesis:_for_t_being_real_number_st_t_in_--_X_holds_
t_>=_-_s
let t be real number ; ::_thesis: ( t in -- X implies t >= - s )
assume  t in -- X ; ::_thesis: t >= - s
then  - t in -- (-- X) by MEMBER_1:11;
then  - t <= s by A2;
then  - (- t) >= - s by XREAL_1:24;
hence  t >= - s ; ::_thesis: verum
end;
then  - (- (lower_bound (-- X))) >= - s by SEQ_4:43;
hence  - (lower_bound (-- X)) <= s by XREAL_1:24; ::_thesis: verum
end;
assume  X is bounded_above ; ::_thesis: upper_bound X = - (lower_bound (-- X))
then A3: -- X is bounded_below by Lm2;
now__::_thesis:_for_t_being_real_number_st_t_in_X_holds_
t_<=_-_(lower_bound_(--_X))
let t be real number ; ::_thesis: ( t in X implies t <= - (lower_bound (-- X)) )
assume  t in X ; ::_thesis: t <= - (lower_bound (-- X))
then  - t in -- X by MEMBER_1:11;
then  - t >= - (- (lower_bound (-- X))) by A3, SEQ_4:def_2;
hence  t <= - (lower_bound (-- X)) by XREAL_1:24; ::_thesis: verum
end;
hence  upper_bound X = - (lower_bound (-- X)) by A1, SEQ_4:46; ::_thesis: verum
end;

Lm4:  for X being Subset of REAL st X is closed holds
-- X is closed
proof
let X be Subset of REAL; ::_thesis: ( X is closed implies -- X is closed )
assume A1: X is closed ; ::_thesis: -- X is closed
let s1 be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng s1 c= -- X or not s1 is convergent or lim s1 in -- X )
assume that
A2: rng s1 c= -- X and
A3: s1 is convergent ; ::_thesis: lim s1 in -- X
A4: - (lim s1) = lim (- s1) by A3, SEQ_2:10;
A5: rng (- s1) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (- s1) or x in X )
assume  x in rng (- s1) ; ::_thesis: x in X
then consider n being set  such that
A6: n in dom (- s1) and
A7: x = (- s1) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
A8: s1 . n in rng s1 by FUNCT_2:4;
 x = - (s1 . n) by A7, SEQ_1:10;
then  x in -- (-- X) by A2, A8;
hence  x in X ; ::_thesis: verum
end;
 - s1 is convergent by A3;
then  lim (- s1) in X by A1, A5, RCOMP_1:def_4;
then  - (- (lim s1)) in -- X by A4, MEMBER_1:11;
hence  lim s1 in -- X ; ::_thesis: verum
end;

theorem :: MEASURE6:45
for X being Subset of REAL holds
( X is closed iff -- X is closed )
proof
let X be Subset of REAL; ::_thesis: ( X is closed iff -- X is closed )
 -- (-- X) = X ;
hence  ( X is closed iff -- X is closed ) by Lm4; ::_thesis: verum
end;

Lm5:  for X being Subset of REAL
for p being Real holds p ++ X =  {  (p + r3) where r3 is Real : r3 in X  }
proof
let X be Subset of REAL; ::_thesis: for p being Real holds p ++ X =  {  (p + r3) where r3 is Real : r3 in X  }
let p be Real; ::_thesis: p ++ X =  {  (p + r3) where r3 is Real : r3 in X  }
thus  p ++ X c=  {  (p + r3) where r3 is Real : r3 in X  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (p + r3) where r3 is Real : r3 in X  }  c= p ++ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in p ++ X or x in  {  (p + r3) where r3 is Real : r3 in X  }  )
assume A1: x in p ++ X ; ::_thesis: x in  {  (p + r3) where r3 is Real : r3 in X  }
then reconsider x9 = x as Real ;
 ex z being Real st
( z in X & x9 = p + z ) by A1, Lm1;
hence  x in  {  (p + r3) where r3 is Real : r3 in X  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (p + r3) where r3 is Real : r3 in X  }  or x in p ++ X )
assume  x in  {  (p + r3) where r3 is Real : r3 in X  }  ; ::_thesis: x in p ++ X
then  ex r3 being Real st
( x = p + r3 & r3 in X ) ;
hence  x in p ++ X by Lm1; ::_thesis: verum
end;

theorem Th46: :: MEASURE6:46
for r being real number
for X being Subset of REAL
for q3 being Real holds
( r in X iff q3 + r in q3 ++ X )
proof
let r be real number ; ::_thesis: for X being Subset of REAL
for q3 being Real holds
( r in X iff q3 + r in q3 ++ X )
let X be Subset of REAL; ::_thesis: for q3 being Real holds
( r in X iff q3 + r in q3 ++ X )
let q3 be Real; ::_thesis: ( r in X iff q3 + r in q3 ++ X )
thus  ( r in X implies q3 + r in q3 ++ X ) by MEMBER_1:141; ::_thesis: ( q3 + r in q3 ++ X implies r in X )
assume  q3 + r in q3 ++ X ; ::_thesis: r in X
then  q3 + r in  {  (q3 + r3) where r3 is Real : r3 in X  }  by Lm5;
then  ex mr being Real st
( q3 + r = q3 + mr & mr in X ) ;
hence  r in X ; ::_thesis: verum
end;

theorem :: MEASURE6:47
for X being Subset of REAL holds X = 0 ++ X by MEMBER_1:146;

theorem :: MEASURE6:48
for X being Subset of REAL
for q3, p3 being Real holds q3 ++ (p3 ++ X) = (q3 + p3) ++ X by MEMBER_1:147;

Lm6:  for X being Subset of REAL
for s being Real st X is bounded_above holds
s ++ X is bounded_above
proof
let X be Subset of REAL; ::_thesis: for s being Real st X is bounded_above holds
s ++ X is bounded_above
let p be Real; ::_thesis: ( X is bounded_above implies p ++ X is bounded_above )
given s being real number  such that A1: s is UpperBound of X ; :: according to XXREAL_2:def_10 ::_thesis: p ++ X is bounded_above
take  p + s ; :: according to XXREAL_2:def_10 ::_thesis: p + s is UpperBound of p ++ X
let t be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not t in p ++ X or t <= p + s )
assume  t in p ++ X ; ::_thesis: t <= p + s
then  t in  {  (p + r3) where r3 is Real : r3 in X  }  by Lm5;
then consider r3 being Real such that
A2: t = p + r3 and
A3: r3 in X ;
 r3 <= s by A1, A3, XXREAL_2:def_1;
hence  t <= p + s by A2, XREAL_1:6; ::_thesis: verum
end;

theorem :: MEASURE6:49
for X being Subset of REAL
for q3 being Real holds
( X is bounded_above iff q3 ++ X is bounded_above )
proof
let X be Subset of REAL; ::_thesis: for q3 being Real holds
( X is bounded_above iff q3 ++ X is bounded_above )
let q3 be Real; ::_thesis: ( X is bounded_above iff q3 ++ X is bounded_above )
(- q3) ++ (q3 ++ X) = ((- q3) + q3) ++ X by MEMBER_1:147
.= X by MEMBER_1:146 ;
hence  ( X is bounded_above iff q3 ++ X is bounded_above ) by Lm6; ::_thesis: verum
end;

Lm7:  for X being Subset of REAL
for p being Real st X is bounded_below holds
p ++ X is bounded_below
proof
let X be Subset of REAL; ::_thesis: for p being Real st X is bounded_below holds
p ++ X is bounded_below
let p be Real; ::_thesis: ( X is bounded_below implies p ++ X is bounded_below )
given s being real number  such that A1: s is LowerBound of X ; :: according to XXREAL_2:def_9 ::_thesis: p ++ X is bounded_below
take  p + s ; :: according to XXREAL_2:def_9 ::_thesis: p + s is LowerBound of p ++ X
let t be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not t in p ++ X or p + s <= t )
assume  t in p ++ X ; ::_thesis: p + s <= t
then  t in  {  (p + r3) where r3 is Real : r3 in X  }  by Lm5;
then consider r3 being Real such that
A2: t = p + r3 and
A3: r3 in X ;
 r3 >= s by A1, A3, XXREAL_2:def_2;
hence  p + s <= t by A2, XREAL_1:6; ::_thesis: verum
end;

theorem :: MEASURE6:50
for X being Subset of REAL
for q3 being Real holds
( X is bounded_below iff q3 ++ X is bounded_below )
proof
let X be Subset of REAL; ::_thesis: for q3 being Real holds
( X is bounded_below iff q3 ++ X is bounded_below )
let q3 be Real; ::_thesis: ( X is bounded_below iff q3 ++ X is bounded_below )
(- q3) ++ (q3 ++ X) = ((- q3) + q3) ++ X by MEMBER_1:147
.= X by MEMBER_1:146 ;
hence  ( X is bounded_below iff q3 ++ X is bounded_below ) by Lm7; ::_thesis: verum
end;

theorem :: MEASURE6:51
for q3 being Real
for X being non empty Subset of REAL st X is bounded_below holds
lower_bound (q3 ++ X) = q3 + (lower_bound X)
proof
let q3 be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below holds
lower_bound (q3 ++ X) = q3 + (lower_bound X)
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below implies lower_bound (q3 ++ X) = q3 + (lower_bound X) )
assume A1: X is bounded_below ; ::_thesis: lower_bound (q3 ++ X) = q3 + (lower_bound X)
set i = q3 + (lower_bound X);
A2: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_q3_++_X_holds_
s_>=_t_)_holds_
t_<=_q3_+_(lower_bound_X)
let t be real number ; ::_thesis: ( ( for s being real number st s in q3 ++ X holds
s >= t ) implies t <= q3 + (lower_bound X) )
assume A3: for s being real number st s in q3 ++ X holds
s >= t ; ::_thesis: t <= q3 + (lower_bound X)
now__::_thesis:_for_s_being_real_number_st_s_in_X_holds_
t_-_q3_<=_s
let s be real number ; ::_thesis: ( s in X implies t - q3 <= s )
assume  s in X ; ::_thesis: t - q3 <= s
then  t <= q3 + s by A3, MEMBER_1:141;
hence  t - q3 <= s by XREAL_1:20; ::_thesis: verum
end;
then  lower_bound X >= t - q3 by SEQ_4:43;
hence  t <= q3 + (lower_bound X) by XREAL_1:20; ::_thesis: verum
end;
now__::_thesis:_for_s_being_real_number_st_s_in_q3_++_X_holds_
s_>=_q3_+_(lower_bound_X)
let s be real number ; ::_thesis: ( s in q3 ++ X implies s >= q3 + (lower_bound X) )
assume  s in q3 ++ X ; ::_thesis: s >= q3 + (lower_bound X)
then  s in  {  (q3 + r3) where r3 is Real : r3 in X  }  by Lm5;
then consider r3 being Real such that
A4: q3 + r3 = s and
A5: r3 in X ;
 r3 >= lower_bound X by A1, A5, SEQ_4:def_2;
hence  s >= q3 + (lower_bound X) by A4, XREAL_1:6; ::_thesis: verum
end;
hence  lower_bound (q3 ++ X) = q3 + (lower_bound X) by A2, SEQ_4:44; ::_thesis: verum
end;

theorem :: MEASURE6:52
for q3 being Real
for X being non empty Subset of REAL st X is bounded_above holds
upper_bound (q3 ++ X) = q3 + (upper_bound X)
proof
let q3 be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above holds
upper_bound (q3 ++ X) = q3 + (upper_bound X)
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above implies upper_bound (q3 ++ X) = q3 + (upper_bound X) )
assume A1: X is bounded_above ; ::_thesis: upper_bound (q3 ++ X) = q3 + (upper_bound X)
set i = q3 + (upper_bound X);
A2: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_q3_++_X_holds_
s_<=_t_)_holds_
q3_+_(upper_bound_X)_<=_t
let t be real number ; ::_thesis: ( ( for s being real number st s in q3 ++ X holds
s <= t ) implies q3 + (upper_bound X) <= t )
assume A3: for s being real number st s in q3 ++ X holds
s <= t ; ::_thesis: q3 + (upper_bound X) <= t
now__::_thesis:_for_s_being_real_number_st_s_in_X_holds_
s_<=_t_-_q3
let s be real number ; ::_thesis: ( s in X implies s <= t - q3 )
assume  s in X ; ::_thesis: s <= t - q3
then  q3 + s <= t by A3, MEMBER_1:141;
hence  s <= t - q3 by XREAL_1:19; ::_thesis: verum
end;
then  upper_bound X <= t - q3 by SEQ_4:45;
hence  q3 + (upper_bound X) <= t by XREAL_1:19; ::_thesis: verum
end;
now__::_thesis:_for_s_being_real_number_st_s_in_q3_++_X_holds_
s_<=_q3_+_(upper_bound_X)
let s be real number ; ::_thesis: ( s in q3 ++ X implies s <= q3 + (upper_bound X) )
assume  s in q3 ++ X ; ::_thesis: s <= q3 + (upper_bound X)
then  s in  {  (q3 + r3) where r3 is Real : r3 in X  }  by Lm5;
then consider r3 being Real such that
A4: q3 + r3 = s and
A5: r3 in X ;
 r3 <= upper_bound X by A1, A5, SEQ_4:def_1;
hence  s <= q3 + (upper_bound X) by A4, XREAL_1:6; ::_thesis: verum
end;
hence  upper_bound (q3 ++ X) = q3 + (upper_bound X) by A2, SEQ_4:46; ::_thesis: verum
end;

Lm8:  for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed
proof
let q3 be Real; ::_thesis: for X being Subset of REAL st X is closed holds
q3 ++ X is closed
let X be Subset of REAL; ::_thesis: ( X is closed implies q3 ++ X is closed )
assume A1: X is closed ; ::_thesis: q3 ++ X is closed
A2: q3 ++ X =  {  (q3 + r3) where r3 is Real : r3 in X  }  by Lm5;
reconsider s0 = NAT --> q3 as Real_Sequence ;
let s1 be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng s1 c= q3 ++ X or not s1 is convergent or lim s1 in q3 ++ X )
assume that
A3: rng s1 c= q3 ++ X and
A4: s1 is convergent ; ::_thesis: lim s1 in q3 ++ X
lim (s1 - s0) = (lim s1) - (s0 . 0) by A4, SEQ_4:42
.= (lim s1) - q3 by FUNCOP_1:7 ;
then A5: q3 + (lim (s1 - s0)) = lim s1 ;
A6: rng (s1 - s0) c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (s1 - s0) or x in X )
assume A7: x in rng (s1 - s0) ; ::_thesis: x in X
then consider n being set  such that
A8: n in dom (s1 - s0) and
A9: x = (s1 - s0) . n by FUNCT_1:def_3;
reconsider x9 = x as Real by A7;
reconsider n = n as Element of NAT by A8;
A10: s1 . n in rng s1 by FUNCT_2:4;
x = (s1 . n) + ((- s0) . n) by A9, SEQ_1:7
.= (s1 . n) + (- (s0 . n)) by SEQ_1:10
.= (s1 . n) - q3 by FUNCOP_1:7 ;
then  x9 + q3 in q3 ++ X by A3, A10;
hence  x in X by Th46; ::_thesis: verum
end;
 s1 - s0 is convergent by A4;
then  lim (s1 - s0) in X by A1, A6, RCOMP_1:def_4;
hence  lim s1 in q3 ++ X by A5, A2; ::_thesis: verum
end;

theorem :: MEASURE6:53
for X being Subset of REAL
for q3 being Real holds
( X is closed iff q3 ++ X is closed )
proof
let X be Subset of REAL; ::_thesis: for q3 being Real holds
( X is closed iff q3 ++ X is closed )
let q3 be Real; ::_thesis: ( X is closed iff q3 ++ X is closed )
(- q3) ++ (q3 ++ X) = ((- q3) + q3) ++ X by MEMBER_1:147
.= X by MEMBER_1:146 ;
hence  ( X is closed iff q3 ++ X is closed ) by Lm8; ::_thesis: verum
end;

definition
let X be Subset of REAL;
func Inv X ->  Subset of REAL equals :: MEASURE6:def 8
 {  (1 / r3) where r3 is Real : r3 in X  }  ;
coherence
  {  (1 / r3) where r3 is Real : r3 in X  }  is Subset of REAL
proof
deffunc H1( Real) ->  Element of REAL = 1 / $1;
defpred S1[ set ] means $1 in X;
thus   {  H1(r3) where r3 is Real : S1[r3]  }  is Subset of REAL from DOMAIN_1:sch_8(); ::_thesis: verum
end;
involutiveness
 for b1, b2 being Subset of REAL st b1 =  {  (1 / r3) where r3 is Real : r3 in b2  }  holds
b2 =  {  (1 / r3) where r3 is Real : r3 in b1  }
proof
let Y, X be Subset of REAL; ::_thesis: ( Y =  {  (1 / r3) where r3 is Real : r3 in X  }  implies X =  {  (1 / r3) where r3 is Real : r3 in Y  }  )
assume A1: Y =  {  (1 / r3) where r3 is Real : r3 in X  }  ; ::_thesis: X =  {  (1 / r3) where r3 is Real : r3 in Y  }
thus  X c=  {  (1 / r3) where r3 is Real : r3 in Y  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (1 / r3) where r3 is Real : r3 in Y  }  c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in  {  (1 / r3) where r3 is Real : r3 in Y  }  )
assume A2: e in X ; ::_thesis: e in  {  (1 / r3) where r3 is Real : r3 in Y  }
then reconsider r = e as Element of REAL ;
A3: 1 / (1 / r) = r ;
 1 / r in Y by A1, A2;
hence  e in  {  (1 / r3) where r3 is Real : r3 in Y  }  by A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (1 / r3) where r3 is Real : r3 in Y  }  or e in X )
assume  e in  {  (1 / r3) where r3 is Real : r3 in Y  }  ; ::_thesis: e in X
then consider r3 being Real such that
A4: e = 1 / r3 and
A5: r3 in Y ;
 ex r1 being Real st
( r3 = 1 / r1 & r1 in X ) by A1, A5;
hence  e in X by A4; ::_thesis: verum
end;
end;

:: deftheorem  defines Inv MEASURE6:def_8_:_
 for X being Subset of REAL holds Inv X =  {  (1 / r3) where r3 is Real : r3 in X  }  ;

theorem Th54: :: MEASURE6:54
for r being real number
for X being Subset of REAL holds
( r in X iff 1 / r in Inv X )
proof
let r be real number ; ::_thesis: for X being Subset of REAL holds
( r in X iff 1 / r in Inv X )
let X be Subset of REAL; ::_thesis: ( r in X iff 1 / r in Inv X )
thus  ( r in X implies 1 / r in Inv X ) ; ::_thesis: ( 1 / r in Inv X implies r in X )
assume  1 / r in Inv X ; ::_thesis: r in X
then  ex mr being Real st
( 1 / r = 1 / mr & mr in X ) ;
hence  r in X by XCMPLX_1:59; ::_thesis: verum
end;

registration
let X be non empty Subset of REAL;
cluster Inv X ->  non empty ;
coherence
 not Inv X is empty
proof
 ex x being Real st x in X by SUBSET_1:4;
hence  not Inv X is empty by Th54; ::_thesis: verum
end;
end;

registration
let X be without_zero Subset of REAL;
cluster Inv X ->  without_zero ;
coherence
 Inv X is without_zero
proof
now__::_thesis:_not_0_in_Inv_X
assume  0 in Inv X ; ::_thesis: contradiction
then  ex r3 being Real st
( 0 = 1 / r3 & r3 in X ) ;
hence  contradiction by XCMPLX_1:202; ::_thesis: verum
end;
hence  Inv X is without_zero by Def2; ::_thesis: verum
end;
end;

theorem :: MEASURE6:55
for X being without_zero Subset of REAL st X is closed & X is real-bounded holds
Inv X is closed
proof
let X be without_zero Subset of REAL; ::_thesis: ( X is closed & X is real-bounded implies Inv X is closed )
assume that
A1: X is closed and
A2: X is real-bounded ; ::_thesis: Inv X is closed
let s1 be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng s1 c= Inv X or not s1 is convergent or lim s1 in Inv X )
assume that
A3: rng s1 c= Inv X and
A4: s1 is convergent ; ::_thesis: lim s1 in Inv X
A5: rng (s1 ") c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (s1 ") or x in X )
assume  x in rng (s1 ") ; ::_thesis: x in X
then consider n being set  such that
A6: n in dom (s1 ") and
A7: x = (s1 ") . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
 s1 . n in rng s1 by FUNCT_2:4;
then  1 / (s1 . n) in Inv (Inv X) by A3;
hence  x in X by A7, VALUED_1:10; ::_thesis: verum
end;
A8: not 0 in rng s1 by A3;
A9: now__::_thesis:_s1_is_non-zero
assume  not s1 is non-zero ; ::_thesis: contradiction
then  ex n being Element of NAT st s1 . n = 0 by SEQ_1:5;
hence  contradiction by A8, FUNCT_2:4; ::_thesis: verum
end;
A10: now__::_thesis:_not_lim_s1_=_0
A11: rng (s1 ") c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (s1 ") or y in X )
assume  y in rng (s1 ") ; ::_thesis: y in X
then consider x being set  such that
A12: x in dom (s1 ") and
A13: y = (s1 ") . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A12;
 s1 . x in rng s1 by FUNCT_2:4;
then  1 / (s1 . x) in Inv (Inv X) by A3;
hence  y in X by A13, VALUED_1:10; ::_thesis: verum
end;
assume  lim s1 = 0 ; ::_thesis: contradiction
then  not s1 " is bounded by A4, A9, Th38;
then  not rng (s1 ") is real-bounded by Th39;
hence  contradiction by A2, A11, XXREAL_2:45; ::_thesis: verum
end;
then  s1 " is convergent by A4, A9, SEQ_2:21;
then  lim (s1 ") in X by A1, A5, RCOMP_1:def_4;
then  1 / (lim s1) in X by A4, A9, A10, SEQ_2:22;
then  1 / (1 / (lim s1)) in Inv X ;
hence  lim s1 in Inv X ; ::_thesis: verum
end;

theorem Th56: :: MEASURE6:56
for Z being Subset-Family of REAL st Z is closed holds
meet Z is closed
proof
let Z be Subset-Family of REAL; ::_thesis: ( Z is closed implies meet Z is closed )
assume A1: Z is closed ; ::_thesis: meet Z is closed
let seq be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng seq c= meet Z or not seq is convergent or lim seq in meet Z )
set mZ = meet Z;
assume that
A2: rng seq c= meet Z and
A3: seq is convergent ; ::_thesis: lim seq in meet Z
percases ( Z = {} or Z <> {} ) ;
suppose Z = {} ; ::_thesis: lim seq in meet Z
then  meet Z = {} by SETFAM_1:def_1;
hence  lim seq in meet Z by A2; ::_thesis: verum
end;
supposeA4: Z <> {} ; ::_thesis: lim seq in meet Z
now__::_thesis:_for_X_being_set_st_X_in_Z_holds_
lim_seq_in_X
let X be set ; ::_thesis: ( X in Z implies lim seq in X )
assume A5: X in Z ; ::_thesis: lim seq in X
then reconsider X9 = X as Subset of REAL ;
A6: rng seq c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng seq or x in X )
assume  x in rng seq ; ::_thesis: x in X
hence  x in X by A2, A5, SETFAM_1:def_1; ::_thesis: verum
end;
 X9 is closed by A1, A5, Def7;
hence  lim seq in X by A3, A6, RCOMP_1:def_4; ::_thesis: verum
end;
hence  lim seq in meet Z by A4, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;

definition
let X be Subset of REAL;
func Cl X ->  Subset of REAL equals :: MEASURE6:def 9
 meet  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
coherence
 meet  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  is Subset of REAL
proof
defpred S1[ Subset of REAL] means ( X c= $1 & $1 is closed );
reconsider Z =  {  A where A is Subset of REAL : S1[A]  }  as Subset-Family of REAL from DOMAIN_1:sch_7();
reconsider Z = Z as Subset-Family of REAL ;
 meet Z is Subset of REAL ;
hence  meet  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  is Subset of REAL ; ::_thesis: verum
end;
projectivity
 for b1, b2 being Subset of REAL st b1 = meet  {  A where A is Subset of REAL : ( b2 c= A & A is closed )  }  holds
b1 = meet  {  A where A is Subset of REAL : ( b1 c= A & A is closed )  }
proof
reconsider W = [#] REAL as Subset of REAL ;
let IT, X be Subset of REAL; ::_thesis: ( IT = meet  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  implies IT = meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  )
set ClX =  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
set ClIT =  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  ;
assume A1: IT = meet  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ; ::_thesis: IT = meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }
A2: W in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
A3: W in  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  ;
thus  IT c= meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  :: according to XBOOLE_0:def_10 ::_thesis: meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  c= IT
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in IT or e in meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  )
assume A4: e in IT ; ::_thesis: e in meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }
 for Y being set st Y in  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  holds
e in Y
proof
let Y be set ; ::_thesis: ( Y in  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  implies e in Y )
assume  Y in  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  ; ::_thesis: e in Y
then consider A being Subset of REAL such that
A5: A = Y and
A6: IT c= A and
A7: A is closed ;
 for Z being set st Z in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  holds
X c= Z
proof
let Z be set ; ::_thesis: ( Z in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  implies X c= Z )
assume  Z in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ; ::_thesis: X c= Z
then  ex B being Subset of REAL st
( Z = B & X c= B & B is closed ) ;
hence  X c= Z ; ::_thesis: verum
end;
then  X c= IT by A1, A2, SETFAM_1:5;
then  X c= A by A6, XBOOLE_1:1;
then  A in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  by A7;
hence  e in Y by A1, A4, A5, SETFAM_1:def_1; ::_thesis: verum
end;
hence  e in meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  by A3, SETFAM_1:def_1; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  or e in IT )
assume A8: e in meet  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  ; ::_thesis: e in IT
 for Y being set st Y in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  holds
e in Y
proof
let Y be set ; ::_thesis: ( Y in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  implies e in Y )
assume A9: Y in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ; ::_thesis: e in Y
then consider A being Subset of REAL such that
A10: A = Y and
 X c= A and
A11: A is closed ;
 IT c= A by A1, A9, A10, SETFAM_1:3;
then  A in  {  A where A is Subset of REAL : ( IT c= A & A is closed )  }  by A11;
hence  e in Y by A8, A10, SETFAM_1:def_1; ::_thesis: verum
end;
hence  e in IT by A1, A2, SETFAM_1:def_1; ::_thesis: verum
end;
end;

:: deftheorem  defines Cl MEASURE6:def_9_:_
 for X being Subset of REAL holds Cl X = meet  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;

registration
let X be Subset of REAL;
cluster Cl X ->  closed ;
coherence
 Cl X is closed
proof
defpred S1[ Subset of REAL] means ( X c= X & X is closed );
reconsider Z =  {  A where A is Subset of REAL : S1[A]  }  as Subset-Family of REAL from DOMAIN_1:sch_7();
reconsider Z = Z as Subset-Family of REAL ;
 Z is closed
proof
let Y be Subset of REAL; :: according to MEASURE6:def_7 ::_thesis: ( Y in Z implies Y is closed )
assume  Y in Z ; ::_thesis: Y is closed
then  ex A being Subset of REAL st
( Y = A & X c= A & A is closed ) ;
hence  Y is closed ; ::_thesis: verum
end;
hence  Cl X is closed by Th56; ::_thesis: verum
end;
end;

theorem Th57: :: MEASURE6:57
for X being Subset of REAL
for Y being closed Subset of REAL st X c= Y holds
Cl X c= Y
proof
let X be Subset of REAL; ::_thesis: for Y being closed Subset of REAL st X c= Y holds
Cl X c= Y
let Y be closed Subset of REAL; ::_thesis: ( X c= Y implies Cl X c= Y )
set ClX =  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
assume  X c= Y ; ::_thesis: Cl X c= Y
then  Y in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
hence  Cl X c= Y by SETFAM_1:3; ::_thesis: verum
end;

theorem Th58: :: MEASURE6:58
for X being Subset of REAL holds X c= Cl X
proof
let X be Subset of REAL; ::_thesis: X c= Cl X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Cl X )
set ClX =  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
assume A1: x in X ; ::_thesis: x in Cl X
A2: now__::_thesis:_for_Y_being_set_st_Y_in__{__A_where_A_is_Subset_of_REAL_:_(_X_c=_A_&_A_is_closed_)__}__holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  implies x in Y )
assume  Y in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ; ::_thesis: x in Y
then  ex YY being Subset of REAL st
( YY = Y & X c= YY & YY is closed ) ;
hence  x in Y by A1; ::_thesis: verum
end;
 [#] REAL in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
hence  x in Cl X by A2, SETFAM_1:def_1; ::_thesis: verum
end;

theorem Th59: :: MEASURE6:59
for X being Subset of REAL holds
( X is closed iff X = Cl X )
proof
let X be Subset of REAL; ::_thesis: ( X is closed iff X = Cl X )
hereby  ::_thesis: ( X = Cl X implies X is closed )
set ClX =  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
assume  X is closed ; ::_thesis: X = Cl X
then  X in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
then A1: Cl X c= X by SETFAM_1:3;
 X c= Cl X by Th58;
hence  X = Cl X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( X = Cl X implies X is closed ) ; ::_thesis: verum
end;

theorem :: MEASURE6:60
Cl ({} REAL) = {} by Th59;

theorem :: MEASURE6:61
Cl ([#] REAL) = REAL by Th59;

theorem :: MEASURE6:62
for X, Y being Subset of REAL st X c= Y holds
Cl X c= Cl Y
proof
let X, Y be Subset of REAL; ::_thesis: ( X c= Y implies Cl X c= Cl Y )
assume A1: X c= Y ; ::_thesis: Cl X c= Cl Y
set ClX =  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
 Y c= Cl Y by Th58;
then  X c= Cl Y by A1, XBOOLE_1:1;
then  Cl Y in  {  A where A is Subset of REAL : ( X c= A & A is closed )  }  ;
hence  Cl X c= Cl Y by SETFAM_1:3; ::_thesis: verum
end;

theorem Th63: :: MEASURE6:63
for X being Subset of REAL
for r3 being Real holds
( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
not O /\ X is empty )
proof
let X be Subset of REAL; ::_thesis: for r3 being Real holds
( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
not O /\ X is empty )
let r3 be Real; ::_thesis: ( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
not O /\ X is empty )
hereby  ::_thesis: ( ( for O being open Subset of REAL st r3 in O holds
not O /\ X is empty ) implies r3 in Cl X )
assume A1: r3 in Cl X ; ::_thesis: for O being open Subset of REAL st r3 in O holds
not O /\ X is empty
let O be open Subset of REAL; ::_thesis: ( r3 in O implies not O /\ X is empty )
assume that
A2: r3 in O and
A3: O /\ X is empty ; ::_thesis: contradiction
 O misses X by A3, XBOOLE_0:def_7;
then A4: X c= O ` by SUBSET_1:23;
A5: O misses O ` by SUBSET_1:24;
 O ` is closed by RCOMP_1:def_5;
then  Cl X c= O ` by A4, Th57;
hence  contradiction by A1, A2, A5, XBOOLE_0:3; ::_thesis: verum
end;
 ((Cl X) `) ` = Cl X ;
then A6: (Cl X) ` is open by RCOMP_1:def_5;
 ( X c= Cl X & ((Cl X) `) /\ X c= X ) by Th58, XBOOLE_1:17;
then A7: ((Cl X) `) /\ X c= Cl X by XBOOLE_1:1;
 ((Cl X) `) /\ X c= (Cl X) ` by XBOOLE_1:17;
then A8: ((Cl X) `) /\ X is empty by A7, SUBSET_1:20;
assume  for O being open Subset of REAL st r3 in O holds
not O /\ X is empty ; ::_thesis: r3 in Cl X
then  not r3 in (Cl X) ` by A6, A8;
hence  r3 in Cl X by SUBSET_1:29; ::_thesis: verum
end;

theorem :: MEASURE6:64
for X being Subset of REAL
for r3 being Real st r3 in Cl X holds
ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )
proof
let X be Subset of REAL; ::_thesis: for r3 being Real st r3 in Cl X holds
ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )
let r3 be Real; ::_thesis: ( r3 in Cl X implies ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 ) )
defpred S1[ set , set ] means  ex n being Nat st
( $1 = n & $2 = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) );
assume A1: r3 in Cl X ; ::_thesis: ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )
A2: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
ex_u_being_set_st_
(_u_in_REAL_&_S1[x,u]_)
let x be set ; ::_thesis: ( x in NAT implies ex u being set st
( u in REAL & S1[x,u] ) )
assume  x in NAT ; ::_thesis: ex u being set st
( u in REAL & S1[x,u] )
then reconsider n = x as Element of NAT ;
set n1 = n + 1;
set oi = ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[;
reconsider u = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) as set ;
take u = u; ::_thesis: ( u in REAL & S1[x,u] )
A3: r3 < r3 + (1 / (n + 1)) by XREAL_1:29;
then  r3 - (1 / (n + 1)) < r3 by XREAL_1:19;
then  r3 in ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ by A3;
then  not X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ is empty by A1, Th63;
then  u in X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ ;
hence  u in REAL ; ::_thesis: S1[x,u]
thus  S1[x,u] ; ::_thesis: verum
end;
consider seq being Function such that
A4: ( dom seq = NAT & rng seq c= REAL ) and
A5: for x being set st x in NAT holds
S1[x,seq . x] from FUNCT_1:sch_5(A2);
reconsider seq = seq as Real_Sequence by A4, FUNCT_2:def_1, RELSET_1:4;
take  seq ; ::_thesis: ( rng seq c= X & seq is convergent & lim seq = r3 )
thus  rng seq c= X ::_thesis: ( seq is convergent & lim seq = r3 )
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng seq or y in X )
assume  y in rng seq ; ::_thesis: y in X
then consider x being set  such that
A6: x in dom seq and
A7: seq . x = y by FUNCT_1:def_3;
consider n being Nat such that
 x = n and
A8: seq . x = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) by A5, A6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
set n1 = n + 1;
set oi = ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[;
A9: r3 < r3 + (1 / (n + 1)) by XREAL_1:29;
then  r3 - (1 / (n + 1)) < r3 by XREAL_1:19;
then  r3 in ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ by A9;
then  not X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ is empty by A1, Th63;
hence  y in X by A7, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
A10: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq_._m)_-_r3)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r3) < p )
set cp = [/(1 / p)\];
A11: 1 / p <= [/(1 / p)\] by INT_1:def_7;
assume A12: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r3) < p
then A13: 0 < [/(1 / p)\] by INT_1:def_7;
then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:3;
take n = cp; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - r3) < p
 n < n + 1 by NAT_1:13;
then A14: 1 / (n + 1) < 1 / n by A13, XREAL_1:88;
 1 / (1 / p) >= 1 / cp by A12, A11, XREAL_1:85;
then A15: 1 / (n + 1) < p by A14, XXREAL_0:2;
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - r3) < p )
assume  n <= m ; ::_thesis: abs ((seq . m) - r3) < p
then A16: n + 1 <= m + 1 by XREAL_1:6;
set m1 = m + 1;
 1 / (m + 1) <= 1 / (n + 1) by A16, XREAL_1:85;
then A17: 1 / (m + 1) < p by A15, XXREAL_0:2;
set oi = ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[;
A18: r3 < r3 + (1 / (m + 1)) by XREAL_1:29;
then  r3 - (1 / (m + 1)) < r3 by XREAL_1:19;
then  r3 in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A18;
then A19: not X /\ ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ is empty by A1, Th63;
 ex m9 being Nat st
( m9 = m & seq . m = choose (X /\ ].(r3 - (1 / (m9 + 1))),(r3 + (1 / (m9 + 1))).[) ) by A5;
then  seq . m in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A19, XBOOLE_0:def_4;
then consider s being Real such that
A20: seq . m = s and
A21: ( r3 - (1 / (m + 1)) < s & s < r3 + (1 / (m + 1)) ) ;
 ( - (1 / (m + 1)) < s - r3 & s - r3 < 1 / (m + 1) ) by A21, XREAL_1:19, XREAL_1:20;
then  abs (s - r3) < 1 / (m + 1) by SEQ_2:1;
hence  abs ((seq . m) - r3) < p by A20, A17, XXREAL_0:2; ::_thesis: verum
end;
hence  seq is convergent by SEQ_2:def_6; ::_thesis: lim seq = r3
hence  lim seq = r3 by A10, SEQ_2:def_7; ::_thesis: verum
end;

begin

definition
let X be set ;
let f be Function of X,REAL;
:: original: bounded_below
redefine attrf is bounded_below  means :: MEASURE6:def 10
f .: X is bounded_below ;
compatibility
 ( f is bounded_below iff f .: X is bounded_below )
proof
A1: dom f = X by FUNCT_2:def_1;
thus  ( f is bounded_below implies f .: X is bounded_below ) ::_thesis: ( f .: X is bounded_below implies f is bounded_below )
proof
given r being real number  such that A2: for y being set st y in dom f holds
r < f . y ; :: according to SEQ_2:def_2 ::_thesis: f .: X is bounded_below
take  r ; :: according to XXREAL_2:def_9 ::_thesis: r is LowerBound of f .: X
let s be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not s in f .: X or r <= s )
assume  s in f .: X ; ::_thesis: r <= s
then  ex x being set st
( x in X & x in X & s = f . x ) by FUNCT_2:64;
hence  r <= s by A1, A2; ::_thesis: verum
end;
given p being real number  such that A3: p is LowerBound of f .: X ; :: according to XXREAL_2:def_9 ::_thesis: f is bounded_below
take  p - 1 ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds
( not b1 in dom f or not f . b1 <= p - 1 )
let y be set ; ::_thesis: ( not y in dom f or not f . y <= p - 1 )
assume  y in dom f ; ::_thesis: not f . y <= p - 1
then  f . y in rng f by FUNCT_1:3;
then  f . y in f .: X by RELSET_1:22;
then A4: p <= f . y by A3, XXREAL_2:def_2;
 f . y < (f . y) + 1 by XREAL_1:29;
then  p < (f . y) + 1 by A4, XXREAL_0:2;
hence  not f . y <= p - 1 by XREAL_1:19; ::_thesis: verum
end;
:: original: bounded_above
redefine attrf is bounded_above  means :: MEASURE6:def 11
f .: X is bounded_above ;
compatibility
 ( f is bounded_above iff f .: X is bounded_above )
proof
A5: dom f = X by FUNCT_2:def_1;
thus  ( f is bounded_above implies f .: X is bounded_above ) ::_thesis: ( f .: X is bounded_above implies f is bounded_above )
proof
given r being real number  such that A6: for y being set st y in dom f holds
r > f . y ; :: according to SEQ_2:def_1 ::_thesis: f .: X is bounded_above
take  r ; :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of f .: X
let s be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not s in f .: X or s <= r )
assume  s in f .: X ; ::_thesis: s <= r
then  ex x being set st
( x in X & x in X & s = f . x ) by FUNCT_2:64;
hence  s <= r by A5, A6; ::_thesis: verum
end;
given p being real number  such that A7: p is UpperBound of f .: X ; :: according to XXREAL_2:def_10 ::_thesis: f is bounded_above
take  p + 1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds
( not b1 in dom f or not p + 1 <= f . b1 )
let y be set ; ::_thesis: ( not y in dom f or not p + 1 <= f . y )
assume  y in dom f ; ::_thesis: not p + 1 <= f . y
then  f . y in rng f by FUNCT_1:3;
then  f . y in f .: X by RELSET_1:22;
then  p >= f . y by A7, XXREAL_2:def_1;
then A8: p + 1 >= (f . y) + 1 by XREAL_1:6;
 f . y < (f . y) + 1 by XREAL_1:29;
hence  not p + 1 <= f . y by A8, XXREAL_0:2; ::_thesis: verum
end;
end;

:: deftheorem  defines bounded_below MEASURE6:def_10_:_
 for X being set
for f being Function of X,REAL holds
( f is bounded_below iff f .: X is bounded_below );

:: deftheorem  defines bounded_above MEASURE6:def_11_:_
 for X being set
for f being Function of X,REAL holds
( f is bounded_above iff f .: X is bounded_above );

definition
let X be set ;
let f be Function of X,REAL;
attrf is with_max  means :: MEASURE6:def 12
f .: X is with_max ;
attrf is with_min  means :: MEASURE6:def 13
f .: X is with_min ;
end;

:: deftheorem  defines with_max MEASURE6:def_12_:_
 for X being set
for f being Function of X,REAL holds
( f is with_max iff f .: X is with_max );

:: deftheorem  defines with_min MEASURE6:def_13_:_
 for X being set
for f being Function of X,REAL holds
( f is with_min iff f .: X is with_min );

theorem Th65: :: MEASURE6:65
for X, A being set
for f being Function of X,REAL holds (- f) .: A = -- (f .: A)
proof
let X, A be set ; ::_thesis: for f being Function of X,REAL holds (- f) .: A = -- (f .: A)
let f be Function of X,REAL; ::_thesis: (- f) .: A = -- (f .: A)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(-_f)_.:_A_implies_x_in_--_(f_.:_A)_)_&_(_x_in_--_(f_.:_A)_implies_x_in_(-_f)_.:_A_)_)
let x be set ; ::_thesis: ( ( x in (- f) .: A implies x in -- (f .: A) ) & ( x in -- (f .: A) implies x in (- f) .: A ) )
hereby  ::_thesis: ( x in -- (f .: A) implies x in (- f) .: A )
assume  x in (- f) .: A ; ::_thesis: x in -- (f .: A)
then consider x1 being set  such that
A1: ( x1 in X & x1 in A & x = (- f) . x1 ) by FUNCT_2:64;
 ( x = - (f . x1) & f . x1 in f .: A ) by A1, FUNCT_2:35, VALUED_1:8;
hence  x in -- (f .: A) ; ::_thesis: verum
end;
assume  x in -- (f .: A) ; ::_thesis: x in (- f) .: A
then consider r3 being Element of COMPLEX  such that
A2: x = - r3 and
A3: r3 in f .: A ;
reconsider r3 = r3 as Real by A3;
consider x1 being set  such that
A4: ( x1 in X & x1 in A ) and
A5: r3 = f . x1 by A3, FUNCT_2:64;
 x = (- f) . x1 by A2, A5, VALUED_1:8;
hence  x in (- f) .: A by A4, FUNCT_2:35; ::_thesis: verum
end;
hence  (- f) .: A = -- (f .: A) by TARSKI:1; ::_thesis: verum
end;

Lm9:  for X being non empty set
for f being Function of X,REAL st f is with_max holds
- f is with_min
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f is with_max holds
- f is with_min
let f be Function of X,REAL; ::_thesis: ( f is with_max implies - f is with_min )
assume that
A1: f .: X is bounded_above and
A2: upper_bound (f .: X) in f .: X ; :: according to MEASURE6:def_4,MEASURE6:def_12 ::_thesis: - f is with_min
A3: -- (f .: X) = (- f) .: X by Th65;
hence  (- f) .: X is bounded_below by A1, Lm2; :: according to MEASURE6:def_5,MEASURE6:def_13 ::_thesis: lower_bound ((- f) .: X) in (- f) .: X
then A4: lower_bound ((- f) .: X) = - (upper_bound (-- (-- (f .: X)))) by A3, Th43
.= - (upper_bound (f .: X)) ;
 - (upper_bound (f .: X)) in -- (f .: X) by A2, MEMBER_1:11;
hence  lower_bound ((- f) .: X) in (- f) .: X by A4, Th65; ::_thesis: verum
end;

Lm10:  for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f is with_min holds
- f is with_max
let f be Function of X,REAL; ::_thesis: ( f is with_min implies - f is with_max )
assume that
A1: f .: X is bounded_below and
A2: lower_bound (f .: X) in f .: X ; :: according to MEASURE6:def_5,MEASURE6:def_13 ::_thesis: - f is with_max
A3: -- (f .: X) = (- f) .: X by Th65;
hence  (- f) .: X is bounded_above by A1, Lm3; :: according to MEASURE6:def_4,MEASURE6:def_12 ::_thesis: upper_bound ((- f) .: X) in (- f) .: X
then A4: upper_bound ((- f) .: X) = - (lower_bound (-- (-- (f .: X)))) by A3, Th44
.= - (lower_bound (f .: X)) ;
 - (lower_bound (f .: X)) in -- (f .: X) by A2, MEMBER_1:11;
hence  upper_bound ((- f) .: X) in (- f) .: X by A4, Th65; ::_thesis: verum
end;

theorem Th66: :: MEASURE6:66
for X being non empty set
for f being Function of X,REAL holds
( f is with_min iff - f is with_max )
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL holds
( f is with_min iff - f is with_max )
let f be Function of X,REAL; ::_thesis: ( f is with_min iff - f is with_max )
 - (- f) = f ;
hence  ( f is with_min iff - f is with_max ) by Lm9, Lm10; ::_thesis: verum
end;

theorem :: MEASURE6:67
for X being non empty set
for f being Function of X,REAL holds
( f is with_max iff - f is with_min )
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL holds
( f is with_max iff - f is with_min )
let f be Function of X,REAL; ::_thesis: ( f is with_max iff - f is with_min )
 - (- f) = f ;
hence  ( f is with_max iff - f is with_min ) by Th66; ::_thesis: verum
end;

theorem :: MEASURE6:68
for X being set
for A being Subset of REAL
for f being Function of X,REAL holds (- f) " A = f " (-- A)
proof
let X be set ; ::_thesis: for A being Subset of REAL
for f being Function of X,REAL holds (- f) " A = f " (-- A)
let A be Subset of REAL; ::_thesis: for f being Function of X,REAL holds (- f) " A = f " (-- A)
let f be Function of X,REAL; ::_thesis: (- f) " A = f " (-- A)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(-_f)_"_A_implies_x_in_f_"_(--_A)_)_&_(_x_in_f_"_(--_A)_implies_x_in_(-_f)_"_A_)_)
let x be set ; ::_thesis: ( ( x in (- f) " A implies x in f " (-- A) ) & ( x in f " (-- A) implies x in (- f) " A ) )
hereby  ::_thesis: ( x in f " (-- A) implies x in (- f) " A )
A1: (- f) . x = - (f . x) by VALUED_1:8;
assume A2: x in (- f) " A ; ::_thesis: x in f " (-- A)
then  (- f) . x in A by FUNCT_2:38;
then  - (- (f . x)) in -- A by A1;
hence  x in f " (-- A) by A2, FUNCT_2:38; ::_thesis: verum
end;
A3: (- f) . x = - (f . x) by VALUED_1:8;
assume A4: x in f " (-- A) ; ::_thesis: x in (- f) " A
then  f . x in -- A by FUNCT_2:38;
then  (- f) . x in -- (-- A) by A3;
hence  x in (- f) " A by A4, FUNCT_2:38; ::_thesis: verum
end;
hence  (- f) " A = f " (-- A) by TARSKI:1; ::_thesis: verum
end;

theorem :: MEASURE6:69
for X, A being set
for f being Function of X,REAL
for s being Real holds (s + f) .: A = s ++ (f .: A)
proof
let X, A be set ; ::_thesis: for f being Function of X,REAL
for s being Real holds (s + f) .: A = s ++ (f .: A)
let f be Function of X,REAL; ::_thesis: for s being Real holds (s + f) .: A = s ++ (f .: A)
let s be Real; ::_thesis: (s + f) .: A = s ++ (f .: A)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(s_+_f)_.:_A_implies_x_in_s_++_(f_.:_A)_)_&_(_x_in_s_++_(f_.:_A)_implies_x_in_(s_+_f)_.:_A_)_)
let x be set ; ::_thesis: ( ( x in (s + f) .: A implies x in s ++ (f .: A) ) & ( x in s ++ (f .: A) implies x in (s + f) .: A ) )
hereby  ::_thesis: ( x in s ++ (f .: A) implies x in (s + f) .: A )
assume  x in (s + f) .: A ; ::_thesis: x in s ++ (f .: A)
then consider x1 being set  such that
A1: ( x1 in X & x1 in A & x = (s + f) . x1 ) by FUNCT_2:64;
 ( x = s + (f . x1) & f . x1 in f .: A ) by A1, FUNCT_2:35, VALUED_1:2;
then  x in  {  (s + q3) where q3 is Real : q3 in f .: A  }  ;
hence  x in s ++ (f .: A) by Lm5; ::_thesis: verum
end;
assume  x in s ++ (f .: A) ; ::_thesis: x in (s + f) .: A
then  x in  {  (s + q3) where q3 is Real : q3 in f .: A  }  by Lm5;
then consider r3 being Real such that
A2: x = s + r3 and
A3: r3 in f .: A ;
consider x1 being set  such that
A4: x1 in X and
A5: x1 in A and
A6: r3 = f . x1 by A3, FUNCT_2:64;
 x = (s + f) . x1 by A2, A4, A6, VALUED_1:2;
hence  x in (s + f) .: A by A4, A5, FUNCT_2:35; ::_thesis: verum
end;
hence  (s + f) .: A = s ++ (f .: A) by TARSKI:1; ::_thesis: verum
end;

theorem :: MEASURE6:70
for X being set
for A being Subset of REAL
for f being Function of X,REAL
for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)
proof
let X be set ; ::_thesis: for A being Subset of REAL
for f being Function of X,REAL
for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)
let A be Subset of REAL; ::_thesis: for f being Function of X,REAL
for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)
let f be Function of X,REAL; ::_thesis: for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)
let q3 be Real; ::_thesis: (q3 + f) " A = f " ((- q3) ++ A)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(q3_+_f)_"_A_implies_x_in_f_"_((-_q3)_++_A)_)_&_(_x_in_f_"_((-_q3)_++_A)_implies_x_in_(q3_+_f)_"_A_)_)
let x be set ; ::_thesis: ( ( x in (q3 + f) " A implies x in f " ((- q3) ++ A) ) & ( x in f " ((- q3) ++ A) implies x in (q3 + f) " A ) )
hereby  ::_thesis: ( x in f " ((- q3) ++ A) implies x in (q3 + f) " A )
assume A1: x in (q3 + f) " A ; ::_thesis: x in f " ((- q3) ++ A)
then  ( (q3 + f) . x in A & (q3 + f) . x = q3 + (f . x) ) by FUNCT_2:38, VALUED_1:2;
then  (- q3) + (q3 + (f . x)) in  {  ((- q3) + p3) where p3 is Real : p3 in A  }  ;
then  (- q3) + (q3 + (f . x)) in (- q3) ++ A by Lm5;
hence  x in f " ((- q3) ++ A) by A1, FUNCT_2:38; ::_thesis: verum
end;
assume A2: x in f " ((- q3) ++ A) ; ::_thesis: x in (q3 + f) " A
then  ( f . x in (- q3) ++ A & (q3 + f) . x = q3 + (f . x) ) by FUNCT_2:38, VALUED_1:2;
then  (q3 + f) . x in  {  (q3 + p3) where p3 is Real : p3 in (- q3) ++ A  }  ;
then  (q3 + f) . x in q3 ++ ((- q3) ++ A) by Lm5;
then  (q3 + f) . x in (q3 + (- q3)) ++ A by MEMBER_1:147;
then  (q3 + f) . x in A by MEMBER_1:146;
hence  x in (q3 + f) " A by A2, FUNCT_2:38; ::_thesis: verum
end;
hence  (q3 + f) " A = f " ((- q3) ++ A) by TARSKI:1; ::_thesis: verum
end;

notation
let f be real-valued Function;
synonym  Inv f for f " ;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: Inv
redefine func Inv f ->  PartFunc of C,REAL;
coherence
 Inv f is PartFunc of C,REAL
proof
 f " is PartFunc of C,REAL ;
hence  Inv f is PartFunc of C,REAL ; ::_thesis: verum
end;
end;

theorem :: MEASURE6:71
for X being set
for A being without_zero Subset of REAL
for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)
proof
let X be set ; ::_thesis: for A being without_zero Subset of REAL
for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)
let A be without_zero Subset of REAL; ::_thesis: for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)
let f be Function of X,REAL; ::_thesis: (Inv f) " A = f " (Inv A)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(Inv_f)_"_A_implies_x_in_f_"_(Inv_A)_)_&_(_x_in_f_"_(Inv_A)_implies_x_in_(Inv_f)_"_A_)_)
let x be set ; ::_thesis: ( ( x in (Inv f) " A implies x in f " (Inv A) ) & ( x in f " (Inv A) implies x in (Inv f) " A ) )
hereby  ::_thesis: ( x in f " (Inv A) implies x in (Inv f) " A )
A1: (Inv f) . x = (f . x) " by VALUED_1:10;
assume A2: x in (Inv f) " A ; ::_thesis: x in f " (Inv A)
then  (Inv f) . x in A by FUNCT_2:38;
then  1 / ((f . x) ") in Inv A by A1;
hence  x in f " (Inv A) by A2, FUNCT_2:38; ::_thesis: verum
end;
A3: ( (f . x) " = 1 / (f . x) & (Inv f) . x = (f . x) " ) by VALUED_1:10;
assume A4: x in f " (Inv A) ; ::_thesis: x in (Inv f) " A
then  f . x in Inv A by FUNCT_2:38;
then  (Inv f) . x in Inv (Inv A) by A3;
hence  x in (Inv f) " A by A4, FUNCT_2:38; ::_thesis: verum
end;
hence  (Inv f) " A = f " (Inv A) by TARSKI:1; ::_thesis: verum
end;

theorem :: MEASURE6:72
for A being Subset of REAL
for x being Real st x in -- A holds
ex a being Real st
( a in A & x = - a )
proof
let A be Subset of REAL; ::_thesis: for x being Real st x in -- A holds
ex a being Real st
( a in A & x = - a )
let x be Real; ::_thesis: ( x in -- A implies ex a being Real st
( a in A & x = - a ) )
assume  x in -- A ; ::_thesis: ex a being Real st
( a in A & x = - a )
then  x in  {  (- a) where a is Element of COMPLEX : a in A  }  ;
then consider a being Element of COMPLEX  such that
A1: ( x = - a & a in A ) ;
reconsider a = a as Real by A1;
take  a ; ::_thesis: ( a in A & x = - a )
thus  ( a in A & x = - a ) by A1; ::_thesis: verum
end;