xxreal_1.miz
begin
reserve x for
set,
p,q,r,s,t,u for
ExtReal,
g for
Real,
a for
Element of
ExtREAL ;
scheme ::
XXREAL_1:sch1
Conti { P,Q[
object] } :
ex s st (for r st P[r] holds r
<= s) & for r st Q[r] holds s
<= r
provided
A1: for r, s st P[r] & Q[s] holds r
<= s;
set A = { a : P[a] }, B = { a : Q[a] };
reconsider X = (A
/\
REAL ), Y = (B
/\
REAL ) as
Subset of
REAL by
XBOOLE_1: 17;
per cases ;
suppose
A2: X
=
{} ;
per cases ;
suppose
A3:
+infty
in A;
take
+infty ;
thus for r st P[r] holds r
<=
+infty by
XXREAL_0: 3;
ex a st a
=
+infty & P[a] by
A3;
hence thesis by
A1;
end;
suppose
A4: not
+infty
in A;
take
-infty ;
thus for r st P[r] holds r
<=
-infty
proof
let r such that
A5: P[r];
r
in
ExtREAL by
XXREAL_0:def 1;
then
A6: r
in A by
A5;
per cases by
A4,
A6,
XXREAL_0: 14;
suppose r
=
-infty ;
hence thesis;
end;
suppose r
in
REAL ;
hence thesis by
A2,
A6,
XBOOLE_0:def 4;
end;
end;
thus thesis by
XXREAL_0: 5;
end;
end;
suppose
A7: Y
=
{} ;
per cases ;
suppose
A8:
-infty
in B;
take
-infty ;
ex a st a
=
-infty & Q[a] by
A8;
hence for r st P[r] holds r
<=
-infty by
A1;
thus thesis by
XXREAL_0: 5;
end;
suppose
A9: not
-infty
in B;
take
+infty ;
thus for r st P[r] holds r
<=
+infty by
XXREAL_0: 3;
let r such that
A10: Q[r];
r
in
ExtREAL by
XXREAL_0:def 1;
then
A11: r
in B by
A10;
per cases by
A9,
A11,
XXREAL_0: 14;
suppose r
=
+infty ;
hence thesis;
end;
suppose r
in
REAL ;
hence thesis by
A7,
A11,
XBOOLE_0:def 4;
end;
end;
end;
suppose that
A12: X
<>
{} and
A13: Y
<>
{} ;
for x,y be
Real st x
in X & y
in Y holds x
<= y
proof
let x,y be
Real;
assume x
in X;
then x
in A by
XBOOLE_0:def 4;
then
A14: ex a st (a
= x) & P[a];
assume y
in Y;
then y
in B by
XBOOLE_0:def 4;
then ex a st a
= y & Q[a];
hence thesis by
A1,
A14;
end;
then
consider s be
Real such that
A15: for x,y be
Real st x
in X & y
in Y holds x
<= s & s
<= y by
AXIOMS: 1;
reconsider s as
ExtReal;
take s;
thus for r st P[r] holds r
<= s
proof
let r;
consider x be
Element of
REAL such that
A16: x
in Y by
A13;
x
in B by
A16,
XBOOLE_0:def 4;
then
A17: ex a st x
= a & Q[a];
assume
A18: P[r];
per cases by
A1,
A17,
A18,
XXREAL_0: 13;
suppose
A19: r
in
REAL ;
then
reconsider r as
Real;
r is
Element of
ExtREAL by
XXREAL_0:def 1;
then r
in A by
A18;
then r
in X by
A19,
XBOOLE_0:def 4;
hence thesis by
A15,
A16;
end;
suppose r
=
-infty ;
hence thesis by
XXREAL_0: 5;
end;
end;
let r;
consider x be
Element of
REAL such that
A20: x
in X by
A12;
x
in A by
A20,
XBOOLE_0:def 4;
then
A21: ex a st x
= a & P[a];
assume
A22: Q[r];
per cases by
A1,
A21,
A22,
XXREAL_0: 10;
suppose
A23: r
in
REAL ;
then
reconsider r as
Real;
r is
Element of
ExtREAL by
XXREAL_0:def 1;
then r
in B by
A22;
then r
in Y by
A23,
XBOOLE_0:def 4;
hence thesis by
A15,
A20;
end;
suppose r
=
+infty ;
hence thesis by
XXREAL_0: 3;
end;
end;
end;
begin
definition
let r,s be
ExtReal;
::
XXREAL_1:def1
func
[.r,s.] ->
set equals { a : r
<= a & a
<= s };
correctness ;
::
XXREAL_1:def2
func
[.r,s.[ ->
set equals { a : r
<= a & a
< s };
correctness ;
::
XXREAL_1:def3
func
].r,s.] ->
set equals { a : r
< a & a
<= s };
correctness ;
::
XXREAL_1:def4
func
].r,s.[ ->
set equals { a : r
< a & a
< s };
correctness ;
end
theorem ::
XXREAL_1:1
Th1: t
in
[.r, s.] iff r
<= t & t
<= s
proof
hereby
assume t
in
[.r, s.];
then ex a st a
= t & r
<= a & a
<= s;
hence r
<= t & t
<= s;
end;
t is
Element of
ExtREAL by
XXREAL_0:def 1;
hence thesis;
end;
theorem ::
XXREAL_1:2
Th2: t
in
].r, s.] iff r
< t & t
<= s
proof
hereby
assume t
in
].r, s.];
then ex a st a
= t & r
< a & a
<= s;
hence r
< t & t
<= s;
end;
t is
Element of
ExtREAL by
XXREAL_0:def 1;
hence thesis;
end;
theorem ::
XXREAL_1:3
Th3: t
in
[.r, s.[ iff r
<= t & t
< s
proof
hereby
assume t
in
[.r, s.[;
then ex a st a
= t & r
<= a & a
< s;
hence r
<= t & t
< s;
end;
t is
Element of
ExtREAL by
XXREAL_0:def 1;
hence thesis;
end;
theorem ::
XXREAL_1:4
Th4: t
in
].r, s.[ iff r
< t & t
< s
proof
hereby
assume t
in
].r, s.[;
then ex a st a
= t & r
< a & a
< s;
hence r
< t & t
< s;
end;
t is
Element of
ExtREAL by
XXREAL_0:def 1;
hence thesis;
end;
registration
let r, s;
cluster
[.r, s.] ->
ext-real-membered;
coherence
proof
let x be
object;
assume x
in
[.r, s.];
then ex a st x
= a & r
<= a & a
<= s;
hence thesis;
end;
cluster
[.r, s.[ ->
ext-real-membered;
coherence
proof
let x be
object;
assume x
in
[.r, s.[;
then ex a st x
= a & r
<= a & a
< s;
hence thesis;
end;
cluster
].r, s.] ->
ext-real-membered;
coherence
proof
let x be
object;
assume x
in
].r, s.];
then ex a st x
= a & r
< a & a
<= s;
hence thesis;
end;
cluster
].r, s.[ ->
ext-real-membered;
coherence
proof
let x be
object;
assume x
in
].r, s.[;
then ex a st x
= a & r
< a & a
< s;
hence thesis;
end;
end
theorem ::
XXREAL_1:5
Th5: x
in
[.p, q.] implies x
in
].p, q.[ or x
= p or x
= q
proof
assume
A1: x
in
[.p, q.];
then
reconsider s = x as
ExtReal;
A2: p
<= s by
A1,
Th1;
A3: s
<= q by
A1,
Th1;
A4: p
= s or p
< s by
A2,
XXREAL_0: 1;
s
= q or s
< q by
A3,
XXREAL_0: 1;
hence thesis by
A4,
Th4;
end;
theorem ::
XXREAL_1:6
Th6: x
in
[.p, q.] implies x
in
].p, q.] or x
= p
proof
assume
A1: x
in
[.p, q.];
then
reconsider s = x as
ExtReal;
A2: p
<= s by
A1,
Th1;
A3: s
<= q by
A1,
Th1;
p
= s or p
< s by
A2,
XXREAL_0: 1;
hence thesis by
A3,
Th2;
end;
theorem ::
XXREAL_1:7
Th7: x
in
[.p, q.] implies x
in
[.p, q.[ or x
= q
proof
assume
A1: x
in
[.p, q.];
then
reconsider s = x as
ExtReal;
A2: p
<= s by
A1,
Th1;
s
<= q by
A1,
Th1;
then q
= s or s
< q by
XXREAL_0: 1;
hence thesis by
A2,
Th3;
end;
theorem ::
XXREAL_1:8
Th8: x
in
[.p, q.[ implies x
in
].p, q.[ or x
= p
proof
assume
A1: x
in
[.p, q.[;
then
reconsider s = x as
ExtReal;
A2: p
<= s by
A1,
Th3;
A3: s
< q by
A1,
Th3;
p
= s or p
< s by
A2,
XXREAL_0: 1;
hence thesis by
A3,
Th4;
end;
theorem ::
XXREAL_1:9
Th9: x
in
].p, q.] implies x
in
].p, q.[ or x
= q
proof
assume
A1: x
in
].p, q.];
then
reconsider s = x as
ExtReal;
A2: p
< s by
A1,
Th2;
s
<= q by
A1,
Th2;
then q
= s or s
< q by
XXREAL_0: 1;
hence thesis by
A2,
Th4;
end;
theorem ::
XXREAL_1:10
x
in
[.p, q.[ implies x
in
].p, q.] & x
<> q or x
= p
proof
assume
A1: x
in
[.p, q.[;
then
reconsider s = x as
ExtReal;
A2: p
<= s by
A1,
Th3;
A3: s
< q by
A1,
Th3;
p
= s or p
< s by
A2,
XXREAL_0: 1;
hence thesis by
A3,
Th2;
end;
theorem ::
XXREAL_1:11
x
in
].p, q.] implies x
in
[.p, q.[ & x
<> p or x
= q
proof
assume
A1: x
in
].p, q.];
then
reconsider s = x as
ExtReal;
A2: p
< s by
A1,
Th2;
s
<= q by
A1,
Th2;
then q
= s or s
< q by
XXREAL_0: 1;
hence thesis by
A2,
Th3;
end;
theorem ::
XXREAL_1:12
Th12: x
in
].p, q.] implies x
in
[.p, q.] & x
<> p
proof
assume
A1: x
in
].p, q.];
then
reconsider s = x as
ExtReal;
A2: p
< s by
A1,
Th2;
s
<= q by
A1,
Th2;
hence thesis by
A2,
Th1;
end;
theorem ::
XXREAL_1:13
Th13: x
in
[.p, q.[ implies x
in
[.p, q.] & x
<> q
proof
assume
A1: x
in
[.p, q.[;
then
reconsider s = x as
ExtReal;
A2: p
<= s by
A1,
Th3;
s
< q by
A1,
Th3;
hence thesis by
A2,
Th1;
end;
theorem ::
XXREAL_1:14
Th14: x
in
].p, q.[ implies x
in
[.p, q.[ & x
<> p
proof
assume
A1: x
in
].p, q.[;
then
reconsider s = x as
ExtReal;
A2: p
< s by
A1,
Th4;
s
< q by
A1,
Th4;
hence thesis by
A2,
Th3;
end;
theorem ::
XXREAL_1:15
Th15: x
in
].p, q.[ implies x
in
].p, q.] & x
<> q
proof
assume
A1: x
in
].p, q.[;
then
reconsider s = x as
ExtReal;
A2: p
< s by
A1,
Th4;
s
< q by
A1,
Th4;
hence thesis by
A2,
Th2;
end;
theorem ::
XXREAL_1:16
Th16: x
in
].p, q.[ implies x
in
[.p, q.] & x
<> p & x
<> q
proof
assume
A1: x
in
].p, q.[;
then x
in
].p, q.] by
Th15;
hence thesis by
A1,
Th12,
Th15;
end;
theorem ::
XXREAL_1:17
Th17:
[.r, r.]
=
{r}
proof
let s;
thus s
in
[.r, r.] implies s
in
{r}
proof
assume s
in
[.r, r.];
then ex a st s
= a & r
<= a & a
<= r;
then s
= r by
XXREAL_0: 1;
hence thesis by
TARSKI:def 1;
end;
assume s
in
{r};
then
A1: s
= r by
TARSKI:def 1;
reconsider s as
Element of
ExtREAL by
XXREAL_0:def 1;
s
<= s;
hence thesis by
A1;
end;
theorem ::
XXREAL_1:18
Th18:
[.r, r.[
=
{}
proof
let p;
not ex p st p
in
[.r, r.[
proof
given p such that
A1: p
in
[.r, r.[;
ex a st p
= a & r
<= a & a
< r by
A1;
hence thesis;
end;
hence thesis;
end;
theorem ::
XXREAL_1:19
Th19:
].r, r.]
=
{}
proof
let p;
thus p
in
].r, r.] implies p
in
{}
proof
assume p
in
].r, r.];
then ex a st p
= a & r
< a & a
<= r;
hence thesis;
end;
thus thesis;
end;
theorem ::
XXREAL_1:20
Th20:
].r, r.[
=
{}
proof
let p;
thus p
in
].r, r.[ implies p
in
{}
proof
assume p
in
].r, r.[;
then ex a st p
= a & r
< a & a
< r;
hence thesis;
end;
thus thesis;
end;
registration
let r;
cluster
[.r, r.] -> non
empty;
coherence
proof
[.r, r.]
=
{r} by
Th17;
hence thesis;
end;
cluster
[.r, r.[ ->
empty;
coherence by
Th18;
cluster
].r, r.] ->
empty;
coherence by
Th19;
cluster
].r, r.[ ->
empty;
coherence by
Th20;
end
theorem ::
XXREAL_1:21
Th21:
].p, q.[
c=
].p, q.]
proof
let s;
assume
A1: s
in
].p, q.[;
then
A2: p
< s by
Th4;
s
< q by
A1,
Th4;
hence thesis by
A2,
Th2;
end;
theorem ::
XXREAL_1:22
Th22:
].p, q.[
c=
[.p, q.[
proof
let s;
assume
A1: s
in
].p, q.[;
then
A2: p
< s by
Th4;
s
< q by
A1,
Th4;
hence thesis by
A2,
Th3;
end;
theorem ::
XXREAL_1:23
Th23:
].p, q.]
c=
[.p, q.]
proof
let s;
assume
A1: s
in
].p, q.];
then
A2: p
< s by
Th2;
s
<= q by
A1,
Th2;
hence thesis by
A2,
Th1;
end;
theorem ::
XXREAL_1:24
Th24:
[.p, q.[
c=
[.p, q.]
proof
let s;
assume
A1: s
in
[.p, q.[;
then
A2: p
<= s by
Th3;
s
< q by
A1,
Th3;
hence thesis by
A2,
Th1;
end;
theorem ::
XXREAL_1:25
Th25:
].p, q.[
c=
[.p, q.]
proof
A1:
].p, q.[
c=
[.p, q.[ by
Th22;
[.p, q.[
c=
[.p, q.] by
Th24;
hence thesis by
A1;
end;
theorem ::
XXREAL_1:26
p
<= q implies
].q, p.]
=
{}
proof
assume
A1: p
<= q;
assume
].q, p.]
<>
{} ;
then
consider r such that
A2: r
in
].q, p.];
A3: q
< r by
A2,
Th2;
r
<= p by
A2,
Th2;
hence contradiction by
A1,
A3,
XXREAL_0: 2;
end;
theorem ::
XXREAL_1:27
Th27: p
<= q implies
[.q, p.[
=
{}
proof
assume
A1: p
<= q;
assume
[.q, p.[
<>
{} ;
then
consider r such that
A2: r
in
[.q, p.[;
A3: q
<= r by
A2,
Th3;
r
< p by
A2,
Th3;
hence contradiction by
A1,
A3,
XXREAL_0: 2;
end;
theorem ::
XXREAL_1:28
Th28: p
<= q implies
].q, p.[
=
{}
proof
assume p
<= q;
then
[.q, p.[
=
{} by
Th27;
hence thesis by
Th22,
XBOOLE_1: 3;
end;
theorem ::
XXREAL_1:29
Th29: p
< q implies
[.q, p.]
=
{}
proof
assume
A1: p
< q;
assume
[.q, p.]
<>
{} ;
then
consider r such that
A2: r
in
[.q, p.];
A3: q
<= r by
A2,
Th1;
r
<= p by
A2,
Th1;
hence contradiction by
A1,
A3,
XXREAL_0: 2;
end;
theorem ::
XXREAL_1:30
r
<= s implies
[.r, s.] is non
empty by
Th1;
theorem ::
XXREAL_1:31
p
< q implies
[.p, q.[ is non
empty by
Th3;
theorem ::
XXREAL_1:32
p
< q implies
].p, q.] is non
empty by
Th2;
theorem ::
XXREAL_1:33
p
< q implies
].p, q.[ is non
empty
proof
assume p
< q;
then ex s st p
< s & s
< q by
XREAL_1: 227;
hence thesis by
Th4;
end;
theorem ::
XXREAL_1:34
Th34: p
<= r & s
<= q implies
[.r, s.]
c=
[.p, q.]
proof
assume that
A1: p
<= r and
A2: s
<= q;
let t;
assume
A3: t
in
[.r, s.];
then
A4: r
<= t by
Th1;
A5: t
<= s by
A3,
Th1;
A6: p
<= t by
A1,
A4,
XXREAL_0: 2;
t
<= q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th1;
end;
theorem ::
XXREAL_1:35
Th35: p
<= r & s
<= q implies
[.r, s.[
c=
[.p, q.]
proof
A1:
[.r, s.[
c=
[.r, s.] by
Th24;
assume that
A2: p
<= r and
A3: s
<= q;
[.r, s.]
c=
[.p, q.] by
A2,
A3,
Th34;
hence thesis by
A1;
end;
theorem ::
XXREAL_1:36
Th36: p
<= r & s
<= q implies
].r, s.]
c=
[.p, q.]
proof
A1:
].r, s.]
c=
[.r, s.] by
Th23;
assume that
A2: p
<= r and
A3: s
<= q;
[.r, s.]
c=
[.p, q.] by
A2,
A3,
Th34;
hence thesis by
A1;
end;
theorem ::
XXREAL_1:37
Th37: p
<= r & s
<= q implies
].r, s.[
c=
[.p, q.]
proof
A1:
].r, s.[
c=
[.r, s.] by
Th25;
assume that
A2: p
<= r and
A3: s
<= q;
[.r, s.]
c=
[.p, q.] by
A2,
A3,
Th34;
hence thesis by
A1;
end;
theorem ::
XXREAL_1:38
Th38: p
<= r & s
<= q implies
[.r, s.[
c=
[.p, q.[
proof
assume that
A1: p
<= r and
A2: s
<= q;
let t;
assume
A3: t
in
[.r, s.[;
then
A4: r
<= t by
Th3;
A5: t
< s by
A3,
Th3;
A6: p
<= t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th3;
end;
theorem ::
XXREAL_1:39
Th39: p
< r & s
<= q implies
[.r, s.]
c=
].p, q.]
proof
assume that
A1: p
< r and
A2: s
<= q;
let t;
assume
A3: t
in
[.r, s.];
then
A4: r
<= t by
Th1;
A5: t
<= s by
A3,
Th1;
A6: p
< t by
A1,
A4,
XXREAL_0: 2;
t
<= q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th2;
end;
theorem ::
XXREAL_1:40
Th40: p
< r & s
<= q implies
[.r, s.[
c=
].p, q.]
proof
A1:
[.r, s.[
c=
[.r, s.] by
Th24;
assume that
A2: p
< r and
A3: s
<= q;
[.r, s.]
c=
].p, q.] by
A2,
A3,
Th39;
hence thesis by
A1;
end;
theorem ::
XXREAL_1:41
Th41: p
<= r & s
<= q implies
].r, s.[
c=
].p, q.]
proof
assume that
A1: p
<= r and
A2: s
<= q;
let t;
assume
A3: t
in
].r, s.[;
then
A4: r
< t by
Th4;
A5: t
< s by
A3,
Th4;
A6: p
< t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th2;
end;
theorem ::
XXREAL_1:42
Th42: p
<= r & s
<= q implies
].r, s.]
c=
].p, q.]
proof
assume that
A1: p
<= r and
A2: s
<= q;
let t;
assume
A3: t
in
].r, s.];
then
A4: r
< t by
Th2;
A5: t
<= s by
A3,
Th2;
A6: p
< t by
A1,
A4,
XXREAL_0: 2;
t
<= q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th2;
end;
theorem ::
XXREAL_1:43
Th43: p
<= r & s
< q implies
[.r, s.]
c=
[.p, q.[
proof
assume that
A1: p
<= r and
A2: s
< q;
let t;
assume
A3: t
in
[.r, s.];
then
A4: r
<= t by
Th1;
A5: t
<= s by
A3,
Th1;
A6: p
<= t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th3;
end;
theorem ::
XXREAL_1:44
Th44: p
<= r & s
< q implies
].r, s.]
c=
[.p, q.[
proof
A1:
].r, s.]
c=
[.r, s.] by
Th23;
assume that
A2: p
<= r and
A3: s
< q;
[.r, s.]
c=
[.p, q.[ by
A2,
A3,
Th43;
hence thesis by
A1;
end;
theorem ::
XXREAL_1:45
Th45: p
<= r & s
<= q implies
].r, s.[
c=
[.p, q.[
proof
assume that
A1: p
<= r and
A2: s
<= q;
let t;
assume
A3: t
in
].r, s.[;
then
A4: r
< t by
Th4;
A5: t
< s by
A3,
Th4;
A6: p
<= t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th3;
end;
theorem ::
XXREAL_1:46
Th46: p
<= r & s
<= q implies
].r, s.[
c=
].p, q.[
proof
assume that
A1: p
<= r and
A2: s
<= q;
let t;
assume
A3: t
in
].r, s.[;
then
A4: r
< t by
Th4;
A5: t
< s by
A3,
Th4;
A6: p
< t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th4;
end;
theorem ::
XXREAL_1:47
Th47: p
< r & s
< q implies
[.r, s.]
c=
].p, q.[
proof
assume that
A1: p
< r and
A2: s
< q;
let t;
assume
A3: t
in
[.r, s.];
then
A4: r
<= t by
Th1;
A5: t
<= s by
A3,
Th1;
A6: p
< t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th4;
end;
theorem ::
XXREAL_1:48
Th48: p
< r & s
<= q implies
[.r, s.[
c=
].p, q.[
proof
assume that
A1: p
< r and
A2: s
<= q;
let t;
assume
A3: t
in
[.r, s.[;
then
A4: r
<= t by
Th3;
A5: t
< s by
A3,
Th3;
A6: p
< t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th4;
end;
theorem ::
XXREAL_1:49
Th49: p
<= r & s
< q implies
].r, s.]
c=
].p, q.[
proof
assume that
A1: p
<= r and
A2: s
< q;
let t;
assume
A3: t
in
].r, s.];
then
A4: r
< t by
Th2;
A5: t
<= s by
A3,
Th2;
A6: p
< t by
A1,
A4,
XXREAL_0: 2;
t
< q by
A2,
A5,
XXREAL_0: 2;
hence thesis by
A6,
Th4;
end;
theorem ::
XXREAL_1:50
Th50: r
<= s &
[.r, s.]
c=
[.p, q.] implies p
<= r & s
<= q
proof
assume
A1: r
<= s;
then
A2: r
in
[.r, s.] by
Th1;
s
in
[.r, s.] by
A1,
Th1;
hence thesis by
A2,
Th1;
end;
theorem ::
XXREAL_1:51
Th51: r
< s &
].r, s.[
c=
[.p, q.] implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
].r, s.[
c=
[.p, q.];
now
let t;
assume that
A3: r
< t and
A4: t
< s;
t
in
].r, s.[ by
A3,
A4,
Th4;
hence p
<= t by
A2,
Th1;
end;
hence p
<= r by
A1,
XREAL_1: 228;
now
let t;
assume that
A5: r
< t and
A6: t
< s;
t
in
].r, s.[ by
A5,
A6,
Th4;
hence t
<= q by
A2,
Th1;
end;
hence thesis by
A1,
XREAL_1: 229;
end;
theorem ::
XXREAL_1:52
Th52: r
< s &
[.r, s.[
c=
[.p, q.] implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
[.r, s.[
c=
[.p, q.];
].r, s.[
c=
[.r, s.[ by
Th22;
then
].r, s.[
c=
[.p, q.] by
A2;
hence thesis by
A1,
Th51;
end;
theorem ::
XXREAL_1:53
Th53: r
< s &
].r, s.]
c=
[.p, q.] implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
].r, s.]
c=
[.p, q.];
].r, s.[
c=
].r, s.] by
Th21;
then
].r, s.[
c=
[.p, q.] by
A2;
hence thesis by
A1,
Th51;
end;
theorem ::
XXREAL_1:54
Th54: r
<= s &
[.r, s.]
c=
[.p, q.[ implies p
<= r & s
< q
proof
assume that
A1: r
<= s and
A2:
[.r, s.]
c=
[.p, q.[;
[.p, q.[
c=
[.p, q.] by
Th24;
then
[.r, s.]
c=
[.p, q.] by
A2;
hence p
<= r by
A1,
Th50;
s
in
[.r, s.] by
A1,
Th1;
hence thesis by
A2,
Th3;
end;
theorem ::
XXREAL_1:55
Th55: r
< s &
[.r, s.[
c=
[.p, q.[ implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
[.r, s.[
c=
[.p, q.[;
].r, s.[
c=
[.r, s.[ by
Th22;
then
A3:
].r, s.[
c=
[.p, q.[ by
A2;
[.p, q.[
c=
[.p, q.] by
Th24;
then
].r, s.[
c=
[.p, q.] by
A3;
hence thesis by
A1,
Th51;
end;
theorem ::
XXREAL_1:56
Th56: r
< s &
].r, s.[
c=
[.p, q.[ implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
].r, s.[
c=
[.p, q.[;
[.p, q.[
c=
[.p, q.] by
Th24;
then
].r, s.[
c=
[.p, q.] by
A2;
hence thesis by
A1,
Th51;
end;
theorem ::
XXREAL_1:57
Th57: r
< s &
].r, s.]
c=
[.p, q.[ implies p
<= r & s
< q
proof
assume that
A1: r
< s and
A2:
].r, s.]
c=
[.p, q.[;
[.p, q.[
c=
[.p, q.] by
Th24;
then
].r, s.]
c=
[.p, q.] by
A2;
hence p
<= r by
A1,
Th53;
s
in
].r, s.] by
A1,
Th2;
hence thesis by
A2,
Th3;
end;
theorem ::
XXREAL_1:58
Th58: r
<= s &
[.r, s.]
c=
].p, q.] implies p
< r & s
<= q
proof
assume that
A1: r
<= s and
A2:
[.r, s.]
c=
].p, q.];
].p, q.]
c=
[.p, q.] by
Th23;
then
A3:
[.r, s.]
c=
[.p, q.] by
A2;
r
in
[.r, s.] by
A1,
Th1;
hence p
< r by
A2,
Th2;
thus thesis by
A1,
A3,
Th50;
end;
theorem ::
XXREAL_1:59
Th59: r
< s &
].r, s.[
c=
].p, q.] implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
].r, s.[
c=
].p, q.];
].p, q.]
c=
[.p, q.] by
Th23;
then
].r, s.[
c=
[.p, q.] by
A2;
hence thesis by
A1,
Th51;
end;
theorem ::
XXREAL_1:60
Th60: r
< s &
[.r, s.[
c=
].p, q.] implies p
< r & s
<= q
proof
assume that
A1: r
< s and
A2:
[.r, s.[
c=
].p, q.];
].p, q.]
c=
[.p, q.] by
Th23;
then
A3:
[.r, s.[
c=
[.p, q.] by
A2;
r
in
[.r, s.[ by
A1,
Th3;
hence p
< r by
A2,
Th2;
thus thesis by
A1,
A3,
Th52;
end;
theorem ::
XXREAL_1:61
Th61: r
< s &
].r, s.]
c=
].p, q.] implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
].r, s.]
c=
].p, q.];
].r, s.[
c=
].r, s.] by
Th21;
then
A3:
].r, s.[
c=
].p, q.] by
A2;
].p, q.]
c=
[.p, q.] by
Th23;
then
].r, s.[
c=
[.p, q.] by
A3;
hence thesis by
A1,
Th51;
end;
theorem ::
XXREAL_1:62
Th62: r
<= s &
[.r, s.]
c=
].p, q.[ implies p
< r & s
< q
proof
assume that
A1: r
<= s and
A2:
[.r, s.]
c=
].p, q.[;
r
in
[.r, s.] by
A1,
Th1;
hence p
< r by
A2,
Th4;
s
in
[.r, s.] by
A1,
Th1;
hence thesis by
A2,
Th4;
end;
theorem ::
XXREAL_1:63
Th63: r
< s &
].r, s.[
c=
].p, q.[ implies p
<= r & s
<= q
proof
assume that
A1: r
< s and
A2:
].r, s.[
c=
].p, q.[;
].p, q.[
c=
[.p, q.] by
Th25;
then
].r, s.[
c=
[.p, q.] by
A2;
hence thesis by
A1,
Th51;
end;
theorem ::
XXREAL_1:64
Th64: r
< s &
[.r, s.[
c=
].p, q.[ implies p
< r & s
<= q
proof
assume that
A1: r
< s and
A2:
[.r, s.[
c=
].p, q.[;
].p, q.[
c=
[.p, q.] by
Th25;
then
A3:
[.r, s.[
c=
[.p, q.] by
A2;
r
in
[.r, s.[ by
A1,
Th3;
hence p
< r by
A2,
Th4;
thus thesis by
A1,
A3,
Th52;
end;
theorem ::
XXREAL_1:65
Th65: r
< s &
].r, s.]
c=
].p, q.[ implies p
<= r & s
< q
proof
assume that
A1: r
< s and
A2:
].r, s.]
c=
].p, q.[;
].p, q.[
c=
[.p, q.] by
Th25;
then
].r, s.]
c=
[.p, q.] by
A2;
hence p
<= r by
A1,
Th53;
s
in
].r, s.] by
A1,
Th2;
hence thesis by
A2,
Th4;
end;
theorem ::
XXREAL_1:66
p
<= q &
[.p, q.]
=
[.r, s.] implies p
= r & q
= s
proof
assume that
A1: p
<= q and
A2:
[.p, q.]
=
[.r, s.];
A3: r
<= p by
A1,
A2,
Th50;
A4: q
<= s by
A1,
A2,
Th50;
r
<= q by
A1,
A3,
XXREAL_0: 2;
then
A5: r
<= s by
A4,
XXREAL_0: 2;
then
A6: p
<= r by
A2,
Th50;
s
<= q by
A2,
A5,
Th50;
hence thesis by
A3,
A4,
A6,
XXREAL_0: 1;
end;
theorem ::
XXREAL_1:67
p
< q &
].p, q.[
=
].r, s.[ implies p
= r & q
= s
proof
assume that
A1: p
< q and
A2:
].p, q.[
=
].r, s.[;
A3: r
<= p by
A1,
A2,
Th63;
A4: q
<= s by
A1,
A2,
Th63;
r
< q by
A1,
A3,
XXREAL_0: 2;
then
A5: r
< s by
A4,
XXREAL_0: 2;
then
A6: p
<= r by
A2,
Th63;
s
<= q by
A2,
A5,
Th63;
hence thesis by
A3,
A4,
A6,
XXREAL_0: 1;
end;
theorem ::
XXREAL_1:68
p
< q &
].p, q.]
=
].r, s.] implies p
= r & q
= s
proof
assume that
A1: p
< q and
A2:
].p, q.]
=
].r, s.];
A3: r
<= p by
A1,
A2,
Th61;
A4: q
<= s by
A1,
A2,
Th61;
r
< q by
A1,
A3,
XXREAL_0: 2;
then
A5: r
< s by
A4,
XXREAL_0: 2;
then
A6: p
<= r by
A2,
Th61;
s
<= q by
A2,
A5,
Th61;
hence thesis by
A3,
A4,
A6,
XXREAL_0: 1;
end;
theorem ::
XXREAL_1:69
p
< q &
[.p, q.[
=
[.r, s.[ implies p
= r & q
= s
proof
assume that
A1: p
< q and
A2:
[.p, q.[
=
[.r, s.[;
A3: r
<= p by
A1,
A2,
Th55;
A4: q
<= s by
A1,
A2,
Th55;
r
< q by
A1,
A3,
XXREAL_0: 2;
then
A5: r
< s by
A4,
XXREAL_0: 2;
then
A6: p
<= r by
A2,
Th55;
s
<= q by
A2,
A5,
Th55;
hence thesis by
A3,
A4,
A6,
XXREAL_0: 1;
end;
theorem ::
XXREAL_1:70
r
<= s implies
[.r, s.]
<>
].p, q.]
proof
assume that
A1: r
<= s and
A2:
[.r, s.]
=
].p, q.];
now
assume r
in
].p, q.];
then
A3: p
< r by
Th2;
s
<= q by
A1,
A2,
Th58;
then r
<= q by
A1,
XXREAL_0: 2;
then p
< q by
A3,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
Th53;
end;
hence contradiction by
A1,
A2,
Th1;
end;
theorem ::
XXREAL_1:71
r
<= s implies
[.r, s.]
<>
[.p, q.[
proof
assume that
A1: r
<= s and
A2:
[.r, s.]
=
[.p, q.[;
now
assume s
in
[.p, q.[;
then
A3: s
< q by
Th3;
p
<= r by
A1,
A2,
Th54;
then p
<= s by
A1,
XXREAL_0: 2;
then p
< q by
A3,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
Th52;
end;
hence contradiction by
A1,
A2,
Th1;
end;
theorem ::
XXREAL_1:72
r
<= s implies
[.r, s.]
<>
].p, q.[
proof
assume that
A1: r
<= s and
A2:
[.r, s.]
=
].p, q.[;
now
assume s
in
].p, q.[;
then
A3: s
< q by
Th4;
p
<= r by
A1,
A2,
Th62;
then p
<= s by
A1,
XXREAL_0: 2;
then p
< q by
A3,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
Th51;
end;
hence contradiction by
A1,
A2,
Th1;
end;
theorem ::
XXREAL_1:73
r
< s implies
[.r, s.[
<>
[.p, q.]
proof
assume that
A1: r
< s and
A2:
[.r, s.[
=
[.p, q.];
A3: not s
in
[.r, s.[ by
Th3;
p
<= r by
A1,
A2,
Th52;
then
A4: p
<= s by
A1,
XXREAL_0: 2;
s
<= q by
A1,
A2,
Th52;
hence contradiction by
A2,
A3,
A4,
Th1;
end;
theorem ::
XXREAL_1:74
r
< s implies
[.r, s.[
<>
].p, q.]
proof
assume that
A1: r
< s and
A2:
[.r, s.[
=
].p, q.];
A3: not s
in
[.r, s.[ by
Th3;
p
<= r by
A1,
A2,
Th60;
then
A4: p
< s by
A1,
XXREAL_0: 2;
s
<= q by
A1,
A2,
Th60;
hence contradiction by
A2,
A3,
A4,
Th2;
end;
theorem ::
XXREAL_1:75
r
< s implies
[.r, s.[
<>
].p, q.[
proof
assume that
A1: r
< s and
A2:
[.r, s.[
=
].p, q.[;
now
assume r
in
].p, q.[;
then
A3: p
< r by
Th4;
s
<= q by
A1,
A2,
Th64;
then r
< q by
A1,
XXREAL_0: 2;
then p
< q by
A3,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
Th56;
end;
hence contradiction by
A1,
A2,
Th3;
end;
theorem ::
XXREAL_1:76
r
< s implies
].r, s.]
<>
[.p, q.]
proof
assume that
A1: r
< s and
A2:
].r, s.]
=
[.p, q.];
A3: not r
in
].r, s.] by
Th2;
A4: p
<= r by
A1,
A2,
Th53;
s
<= q by
A1,
A2,
Th53;
then r
<= q by
A1,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
A4,
Th1;
end;
theorem ::
XXREAL_1:77
r
< s implies
].r, s.]
<>
[.p, q.[
proof
assume that
A1: r
< s and
A2:
].r, s.]
=
[.p, q.[;
A3: not r
in
].r, s.] by
Th2;
A4: p
<= r by
A1,
A2,
Th57;
s
<= q by
A1,
A2,
Th57;
then r
< q by
A1,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
A4,
Th3;
end;
theorem ::
XXREAL_1:78
r
< s implies
].r, s.]
<>
].p, q.[
proof
assume that
A1: r
< s and
A2:
].r, s.]
=
].p, q.[;
now
assume s
in
].p, q.[;
then
A3: s
< q by
Th4;
p
<= r by
A1,
A2,
Th65;
then p
<= s by
A1,
XXREAL_0: 2;
then p
< q by
A3,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
Th59;
end;
hence contradiction by
A1,
A2,
Th2;
end;
theorem ::
XXREAL_1:79
r
< s implies
].r, s.[
<>
[.p, q.]
proof
assume that
A1: r
< s and
A2:
].r, s.[
=
[.p, q.];
A3: not r
in
].r, s.[ by
Th4;
A4: p
<= r by
A1,
A2,
Th51;
s
<= q by
A1,
A2,
Th51;
then r
<= q by
A1,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
A4,
Th1;
end;
theorem ::
XXREAL_1:80
r
< s implies
].r, s.[
<>
].p, q.]
proof
assume that
A1: r
< s and
A2:
].r, s.[
=
].p, q.];
A3: not s
in
].r, s.[ by
Th4;
p
<= r by
A1,
A2,
Th59;
then
A4: p
< s by
A1,
XXREAL_0: 2;
s
<= q by
A1,
A2,
Th59;
hence contradiction by
A2,
A3,
A4,
Th2;
end;
theorem ::
XXREAL_1:81
r
< s implies
].r, s.[
<>
[.p, q.[
proof
assume that
A1: r
< s and
A2:
].r, s.[
=
[.p, q.[;
A3: not r
in
].r, s.[ by
Th4;
A4: p
<= r by
A1,
A2,
Th56;
s
<= q by
A1,
A2,
Th56;
then r
< q by
A1,
XXREAL_0: 2;
hence contradiction by
A2,
A3,
A4,
Th3;
end;
theorem ::
XXREAL_1:82
r
<= s &
[.r, s.]
c<
[.p, q.] implies p
< r or s
< q
proof
assume
A1: r
<= s;
assume
A2:
[.r, s.]
c<
[.p, q.];
then
A3:
[.r, s.]
c=
[.p, q.];
then
A4: p
<= r by
A1,
Th50;
A5: s
<= q by
A1,
A3,
Th50;
p
<> r or s
<> q by
A2;
hence thesis by
A4,
A5,
XXREAL_0: 1;
end;
theorem ::
XXREAL_1:83
r
< s &
].r, s.[
c=
[.p, q.] implies
[.r, s.]
c=
[.p, q.]
proof
assume that
A1: r
< s and
A2:
].r, s.[
c=
[.p, q.];
let t;
assume
A3: t
in
[.r, s.];
per cases by
A3,
Th5;
suppose t
in
].r, s.[;
hence thesis by
A2;
end;
suppose
A4: t
= r;
then
A5: p
<= t by
A1,
A2,
Th51;
s
<= q by
A1,
A2,
Th51;
then t
<= q by
A1,
A4,
XXREAL_0: 2;
hence thesis by
A5,
Th1;
end;
suppose
A6: t
= s;
A7: s
<= q by
A1,
A2,
Th51;
p
<= r by
A1,
A2,
Th51;
then p
<= t by
A1,
A6,
XXREAL_0: 2;
hence thesis by
A6,
A7,
Th1;
end;
end;
theorem ::
XXREAL_1:84
r
< s implies
[.s, p.[
c=
].r, p.[
proof
assume
A1: r
< s;
let t;
assume
A2: t
in
[.s, p.[;
then s
<= t by
Th3;
then
A3: r
< t by
A1,
XXREAL_0: 2;
t
< p by
A2,
Th3;
hence thesis by
A3,
Th4;
end;
theorem ::
XXREAL_1:85
Th85: s
<= r implies
[.r, s.]
c=
{r} &
[.r, s.]
c=
{s}
proof
assume
A1: s
<= r;
thus
[.r, s.]
c=
{r}
proof
let t;
assume
A2: t
in
[.r, s.];
then
A3: t
<= s by
Th1;
A4: r
<= t by
A2,
Th1;
t
<= r by
A1,
A3,
XXREAL_0: 2;
then r
= t by
A4,
XXREAL_0: 1;
hence thesis by
TARSKI:def 1;
end;
let t;
assume
A5: t
in
[.r, s.];
then r
<= t by
Th1;
then
A6: s
<= t by
A1,
XXREAL_0: 2;
t
<= s by
A5,
Th1;
then s
= t by
A6,
XXREAL_0: 1;
hence thesis by
TARSKI:def 1;
end;
theorem ::
XXREAL_1:86
].r, s.[
misses
{r, s}
proof
let t;
assume
A1: t
in
].r, s.[;
then
A2: r
< t by
Th4;
t
< s by
A1,
Th4;
hence thesis by
A2,
TARSKI:def 2;
end;
theorem ::
XXREAL_1:87
[.r, s.[
misses
{s}
proof
let t;
assume t
in
[.r, s.[;
then t
< s by
Th3;
hence thesis by
TARSKI:def 1;
end;
theorem ::
XXREAL_1:88
].r, s.]
misses
{r}
proof
let t;
assume t
in
].r, s.];
then r
< t by
Th2;
hence thesis by
TARSKI:def 1;
end;
theorem ::
XXREAL_1:89
s
<= p implies
[.r, s.]
misses
].p, q.[
proof
assume
A1: s
<= p;
let t;
assume t
in
[.r, s.];
then t
<= s by
Th1;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th4;
end;
theorem ::
XXREAL_1:90
s
<= p implies
[.r, s.]
misses
].p, q.]
proof
assume
A1: s
<= p;
let t;
assume t
in
[.r, s.];
then t
<= s by
Th1;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th2;
end;
theorem ::
XXREAL_1:91
s
<= p implies
].r, s.]
misses
].p, q.[
proof
assume
A1: s
<= p;
let t;
assume t
in
].r, s.];
then t
<= s by
Th2;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th4;
end;
theorem ::
XXREAL_1:92
s
<= p implies
].r, s.]
misses
].p, q.]
proof
assume
A1: s
<= p;
let t;
assume t
in
].r, s.];
then t
<= s by
Th2;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th2;
end;
theorem ::
XXREAL_1:93
s
<= p implies
].r, s.[
misses
[.p, q.]
proof
assume
A1: s
<= p;
let t;
assume t
in
].r, s.[;
then t
< s by
Th4;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th1;
end;
theorem ::
XXREAL_1:94
s
<= p implies
].r, s.[
misses
[.p, q.[
proof
assume
A1: s
<= p;
let t;
assume t
in
].r, s.[;
then t
< s by
Th4;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th3;
end;
theorem ::
XXREAL_1:95
s
<= p implies
[.r, s.[
misses
[.p, q.]
proof
assume
A1: s
<= p;
let t;
assume t
in
[.r, s.[;
then t
< s by
Th3;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th1;
end;
theorem ::
XXREAL_1:96
s
<= p implies
[.r, s.[
misses
[.p, q.[
proof
assume
A1: s
<= p;
let t;
assume t
in
[.r, s.[;
then t
< s by
Th3;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th3;
end;
theorem ::
XXREAL_1:97
r
< p & r
< s implies not
].r, s.[
c=
[.p, q.]
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A4,
A5,
Th4;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th1;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A7,
Th4;
thus thesis by
A8,
Th1;
end;
end;
theorem ::
XXREAL_1:98
r
< p & r
< s implies not
[.r, s.[
c=
[.p, q.]
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
[.r, s.[ by
A4,
A5,
Th3;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th1;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
[.r, s.[ by
A7,
Th3;
thus thesis by
A8,
Th1;
end;
end;
theorem ::
XXREAL_1:99
r
< p & r
< s implies not
].r, s.]
c=
[.p, q.]
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.] by
A4,
A5,
Th2;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th1;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.] by
A7,
Th2;
thus thesis by
A8,
Th1;
end;
end;
theorem ::
XXREAL_1:100
r
< p & r
<= s implies not
[.r, s.]
c=
[.p, q.]
proof
assume that
A1: r
< p and
A2: r
<= s;
take t = r;
thus t
in
[.r, s.] by
A2,
Th1;
thus thesis by
A1,
Th1;
end;
theorem ::
XXREAL_1:101
r
< p & r
< s implies not
].r, s.[
c=
[.p, q.[
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A4,
A5,
Th4;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th3;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A7,
Th4;
thus thesis by
A8,
Th3;
end;
end;
theorem ::
XXREAL_1:102
r
< p & r
< s implies not
].r, s.]
c=
[.p, q.[
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.] by
A4,
A5,
Th2;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th3;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.] by
A7,
Th2;
thus thesis by
A8,
Th3;
end;
end;
theorem ::
XXREAL_1:103
r
< p & r
< s implies not
[.r, s.[
c=
[.p, q.[
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
[.r, s.[ by
A4,
A5,
Th3;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th3;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
[.r, s.[ by
A7,
Th3;
thus thesis by
A8,
Th3;
end;
end;
theorem ::
XXREAL_1:104
r
< p & r
<= s implies not
[.r, s.]
c=
[.p, q.[
proof
assume that
A1: r
< p and
A2: r
<= s;
take t = r;
thus t
in
[.r, s.] by
A2,
Th1;
thus thesis by
A1,
Th3;
end;
theorem ::
XXREAL_1:105
r
< p & r
< s implies not
].r, s.[
c=
].p, q.]
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A4,
A5,
Th4;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th2;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A7,
Th4;
thus thesis by
A8,
Th2;
end;
end;
theorem ::
XXREAL_1:106
r
<= p & r
< s implies not
[.r, s.[
c=
].p, q.]
proof
assume that
A1: r
<= p and
A2: r
< s;
take t = r;
thus t
in
[.r, s.[ by
A2,
Th3;
thus thesis by
A1,
Th2;
end;
theorem ::
XXREAL_1:107
r
< p & r
< s implies not
].r, s.]
c=
].p, q.]
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.] by
A4,
A5,
Th2;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th2;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
<= s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.] by
A7,
Th2;
thus thesis by
A8,
Th2;
end;
end;
theorem ::
XXREAL_1:108
r
<= p & r
<= s implies not
[.r, s.]
c=
].p, q.]
proof
assume that
A1: r
<= p and
A2: r
<= s;
take r;
thus r
in
[.r, s.] by
A2,
Th1;
thus thesis by
A1,
Th2;
end;
theorem ::
XXREAL_1:109
r
<= p & r
<= s implies not
[.r, s.]
c=
].p, q.[
proof
assume that
A1: r
<= p and
A2: r
<= s;
take r;
thus r
in
[.r, s.] by
A2,
Th1;
thus thesis by
A1,
Th4;
end;
theorem ::
XXREAL_1:110
r
<= p & r
< s implies not
[.r, s.[
c=
].p, q.[
proof
assume that
A1: r
<= p and
A2: r
< s;
take r;
thus r
in
[.r, s.[ by
A2,
Th3;
thus thesis by
A1,
Th4;
end;
theorem ::
XXREAL_1:111
r
< p & r
< s implies not
].r, s.]
c=
].p, q.[
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.] by
A4,
A5,
Th2;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th4;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
<= s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.] by
A7,
Th2;
thus thesis by
A8,
Th4;
end;
end;
theorem ::
XXREAL_1:112
r
< p & r
< s implies not
].r, s.[
c=
].p, q.[
proof
assume that
A1: r
< p and
A2: r
< s;
per cases ;
suppose
A3: s
<= p;
consider t such that
A4: r
< t and
A5: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A4,
A5,
Th4;
t
< p by
A3,
A5,
XXREAL_0: 2;
hence thesis by
Th4;
end;
suppose
A6: p
<= s;
consider t such that
A7: r
< t and
A8: t
< p by
A1,
XREAL_1: 227;
take t;
t
< s by
A6,
A8,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A7,
Th4;
thus thesis by
A8,
Th4;
end;
end;
theorem ::
XXREAL_1:113
q
< s & r
< s implies not
].r, s.[
c=
[.p, q.]
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A5,
Th4;
thus thesis by
A4,
Th1;
end;
suppose
A6: q
<= r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A7,
A8,
Th4;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th1;
end;
end;
theorem ::
XXREAL_1:114
q
< s & r
< s implies not
[.r, s.[
c=
[.p, q.]
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
[.r, s.[ by
A5,
Th3;
thus thesis by
A4,
Th1;
end;
suppose
A6: q
<= r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
[.r, s.[ by
A7,
A8,
Th3;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th1;
end;
end;
theorem ::
XXREAL_1:115
q
< s & r
< s implies not
].r, s.]
c=
[.p, q.]
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
].r, s.] by
A5,
Th2;
thus thesis by
A4,
Th1;
end;
suppose
A6: q
<= r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.] by
A7,
A8,
Th2;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th1;
end;
end;
theorem ::
XXREAL_1:116
q
< s & r
<= s implies not
[.r, s.]
c=
[.p, q.]
proof
assume that
A1: q
< s and
A2: r
<= s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
[.r, s.] by
A5,
Th1;
thus thesis by
A4,
Th1;
end;
suppose
A6: q
< r;
take t = r;
thus t
in
[.r, s.] by
A2,
Th1;
thus thesis by
A6,
Th1;
end;
end;
theorem ::
XXREAL_1:117
q
< s & r
< s implies not
].r, s.[
c=
[.p, q.[
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A5,
Th4;
thus thesis by
A4,
Th3;
end;
suppose
A6: q
< r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A7,
A8,
Th4;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th3;
end;
end;
theorem ::
XXREAL_1:118
q
<= s & r
< s implies not
].r, s.]
c=
[.p, q.[
proof
assume that
A1: q
<= s and
A2: r
< s;
take t = s;
thus t
in
].r, s.] by
A2,
Th2;
thus thesis by
A1,
Th3;
end;
theorem ::
XXREAL_1:119
q
< s & r
< s implies not
[.r, s.[
c=
[.p, q.[
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
[.r, s.[ by
A5,
Th3;
thus thesis by
A4,
Th3;
end;
suppose
A6: q
< r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
[.r, s.[ by
A7,
A8,
Th3;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th3;
end;
end;
theorem ::
XXREAL_1:120
q
< s & r
< s implies not
].r, s.[
c=
].p, q.]
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A5,
Th4;
thus thesis by
A4,
Th2;
end;
suppose
A6: q
< r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A7,
A8,
Th4;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th2;
end;
end;
theorem ::
XXREAL_1:121
q
< s & r
<= s implies not
[.r, s.]
c=
].p, q.]
proof
assume that
A1: q
< s and
A2: r
<= s;
take t = s;
thus t
in
[.r, s.] by
A2,
Th1;
thus thesis by
A1,
Th2;
end;
theorem ::
XXREAL_1:122
q
< s & r
< s implies not
[.r, s.[
c=
].p, q.]
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
[.r, s.[ by
A5,
Th3;
thus thesis by
A4,
Th2;
end;
suppose
A6: q
< r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
[.r, s.[ by
A7,
A8,
Th3;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th2;
end;
end;
theorem ::
XXREAL_1:123
q
< s & r
< s implies not
].r, s.]
c=
].p, q.]
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
].r, s.] by
A5,
Th2;
thus thesis by
A4,
Th2;
end;
suppose
A6: q
< r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.] by
A7,
A8,
Th2;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th2;
end;
end;
theorem ::
XXREAL_1:124
q
<= s & r
<= s implies not
[.r, s.]
c=
].p, q.[
proof
assume that
A1: q
<= s and
A2: r
<= s;
take t = s;
thus t
in
[.r, s.] by
A2,
Th1;
thus thesis by
A1,
Th4;
end;
theorem ::
XXREAL_1:125
q
< s & r
< s implies not
[.r, s.[
c=
].p, q.[
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
[.r, s.[ by
A5,
Th3;
thus thesis by
A4,
Th4;
end;
suppose
A6: q
< r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
[.r, s.[ by
A7,
A8,
Th3;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th4;
end;
end;
theorem ::
XXREAL_1:126
q
<= s & r
< s implies not
].r, s.]
c=
].p, q.[
proof
assume that
A1: q
<= s and
A2: r
< s;
take t = s;
thus t
in
].r, s.] by
A2,
Th2;
thus thesis by
A1,
Th4;
end;
theorem ::
XXREAL_1:127
q
< s & r
< s implies not
].r, s.[
c=
].p, q.[
proof
assume that
A1: q
< s and
A2: r
< s;
per cases ;
suppose
A3: r
<= q;
consider t such that
A4: q
< t and
A5: t
< s by
A1,
XREAL_1: 227;
take t;
r
< t by
A3,
A4,
XXREAL_0: 2;
hence t
in
].r, s.[ by
A5,
Th4;
thus thesis by
A4,
Th4;
end;
suppose
A6: q
< r;
consider t such that
A7: r
< t and
A8: t
< s by
A2,
XREAL_1: 227;
take t;
thus t
in
].r, s.[ by
A7,
A8,
Th4;
q
< t by
A6,
A7,
XXREAL_0: 2;
hence thesis by
Th4;
end;
end;
begin
theorem ::
XXREAL_1:128
Th128: r
<= s implies
[.r, s.]
= (
].r, s.[
\/
{r, s})
proof
assume
A1: r
<= s;
let t;
thus t
in
[.r, s.] implies t
in (
].r, s.[
\/
{r, s})
proof
assume t
in
[.r, s.];
then t
in
].r, s.[ or t
= r or t
= s by
Th5;
then t
in
].r, s.[ or t
in
{r, s} by
TARSKI:def 2;
hence thesis by
XBOOLE_0:def 3;
end;
assume t
in (
].r, s.[
\/
{r, s});
then t
in
].r, s.[ or t
in
{r, s} by
XBOOLE_0:def 3;
then t
in
].r, s.[ or t
= r or t
= s by
TARSKI:def 2;
hence thesis by
A1,
Th1,
Th16;
end;
theorem ::
XXREAL_1:129
Th129: r
<= s implies
[.r, s.]
= (
[.r, s.[
\/
{s})
proof
assume
A1: r
<= s;
let t;
thus t
in
[.r, s.] implies t
in (
[.r, s.[
\/
{s})
proof
assume t
in
[.r, s.];
then t
in
[.r, s.[ or t
= s by
Th7;
then t
in
[.r, s.[ or t
in
{s} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
assume t
in (
[.r, s.[
\/
{s});
then t
in
[.r, s.[ or t
in
{s} by
XBOOLE_0:def 3;
then t
in
[.r, s.[ or t
= s by
TARSKI:def 1;
hence thesis by
A1,
Th1,
Th13;
end;
theorem ::
XXREAL_1:130
Th130: r
<= s implies
[.r, s.]
= (
{r}
\/
].r, s.])
proof
assume
A1: r
<= s;
let t;
thus t
in
[.r, s.] implies t
in (
{r}
\/
].r, s.])
proof
assume t
in
[.r, s.];
then t
in
].r, s.] or t
= r by
Th6;
then t
in
].r, s.] or t
in
{r} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
assume t
in (
{r}
\/
].r, s.]);
then t
in
].r, s.] or t
in
{r} by
XBOOLE_0:def 3;
then t
in
].r, s.] or t
= r by
TARSKI:def 1;
hence thesis by
A1,
Th1,
Th12;
end;
theorem ::
XXREAL_1:131
Th131: r
< s implies
[.r, s.[
= (
{r}
\/
].r, s.[)
proof
assume
A1: r
< s;
let t;
thus t
in
[.r, s.[ implies t
in (
{r}
\/
].r, s.[)
proof
assume t
in
[.r, s.[;
then t
in
].r, s.[ or t
= r by
Th8;
then t
in
].r, s.[ or t
in
{r} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
assume t
in (
{r}
\/
].r, s.[);
then t
in
].r, s.[ or t
in
{r} by
XBOOLE_0:def 3;
then t
in
].r, s.[ or t
= r by
TARSKI:def 1;
hence thesis by
A1,
Th3,
Th14;
end;
theorem ::
XXREAL_1:132
Th132: r
< s implies
].r, s.]
= (
].r, s.[
\/
{s})
proof
assume
A1: r
< s;
let t;
thus t
in
].r, s.] implies t
in (
].r, s.[
\/
{s})
proof
assume t
in
].r, s.];
then t
in
].r, s.[ or t
= s by
Th9;
then t
in
].r, s.[ or t
in
{s} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
assume t
in (
].r, s.[
\/
{s});
then t
in
].r, s.[ or t
in
{s} by
XBOOLE_0:def 3;
then t
in
].r, s.[ or t
= s by
TARSKI:def 1;
hence thesis by
A1,
Th2,
Th15;
end;
theorem ::
XXREAL_1:133
r
<= s implies (
[.r, s.]
\
{r, s})
=
].r, s.[
proof
assume r
<= s;
then
A1:
[.r, s.]
= (
].r, s.[
\/
{r, s}) by
Th128;
A2: not r
in
].r, s.[ by
Th4;
not s
in
].r, s.[ by
Th4;
hence thesis by
A1,
A2,
ZFMISC_1: 121;
end;
theorem ::
XXREAL_1:134
r
<= s implies (
[.r, s.]
\
{r})
=
].r, s.]
proof
assume r
<= s;
then
A1:
[.r, s.]
= (
{r}
\/
].r, s.]) by
Th130;
not r
in
].r, s.] by
Th2;
hence thesis by
A1,
ZFMISC_1: 117;
end;
theorem ::
XXREAL_1:135
r
<= s implies (
[.r, s.]
\
{s})
=
[.r, s.[
proof
assume r
<= s;
then
A1:
[.r, s.]
= (
[.r, s.[
\/
{s}) by
Th129;
not s
in
[.r, s.[ by
Th3;
hence thesis by
A1,
ZFMISC_1: 117;
end;
theorem ::
XXREAL_1:136
r
< s implies (
[.r, s.[
\
{r})
=
].r, s.[
proof
assume r
< s;
then
A1:
[.r, s.[
= (
{r}
\/
].r, s.[) by
Th131;
not r
in
].r, s.[ by
Th4;
hence thesis by
A1,
ZFMISC_1: 117;
end;
theorem ::
XXREAL_1:137
r
< s implies (
].r, s.]
\
{s})
=
].r, s.[
proof
assume r
< s;
then
A1:
].r, s.]
= (
].r, s.[
\/
{s}) by
Th132;
not s
in
].r, s.[ by
Th4;
hence thesis by
A1,
ZFMISC_1: 117;
end;
theorem ::
XXREAL_1:138
r
< s & s
< t implies (
].r, s.]
/\
[.s, t.[)
=
{s}
proof
assume that
A1: r
< s and
A2: s
< t;
now
let x be
object;
hereby
assume
A3: x
in (
].r, s.]
/\
[.s, t.[);
then
reconsider p = x as
ExtReal;
A4: p
in
].r, s.] by
A3,
XBOOLE_0:def 4;
p
in
[.s, t.[ by
A3,
XBOOLE_0:def 4;
then
A5: s
<= p by
Th3;
p
<= s by
A4,
Th2;
hence x
= s by
A5,
XXREAL_0: 1;
end;
assume
A6: x
= s;
A7: s
in
].r, s.] by
A1,
Th2;
s
in
[.s, t.[ by
A2,
Th3;
hence x
in (
].r, s.]
/\
[.s, t.[) by
A6,
A7,
XBOOLE_0:def 4;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
XXREAL_1:139
(
[.r, s.[
/\
[.p, q.[)
=
[.(
max (r,p)), (
min (s,q)).[
proof
let t;
thus t
in (
[.r, s.[
/\
[.p, q.[) implies t
in
[.(
max (r,p)), (
min (s,q)).[
proof
assume
A1: t
in (
[.r, s.[
/\
[.p, q.[);
then
A2: t
in
[.r, s.[ by
XBOOLE_0:def 4;
A3: t
in
[.p, q.[ by
A1,
XBOOLE_0:def 4;
A4: r
<= t by
A2,
Th3;
A5: t
< s by
A2,
Th3;
A6: p
<= t by
A3,
Th3;
A7: t
< q by
A3,
Th3;
A8: (
max (r,p))
<= t by
A4,
A6,
XXREAL_0: 28;
t
< (
min (s,q)) by
A5,
A7,
XXREAL_0: 21;
hence thesis by
A8,
Th3;
end;
assume
A9: t
in
[.(
max (r,p)), (
min (s,q)).[;
then
A10: (
max (r,p))
<= t by
Th3;
A11: t
< (
min (s,q)) by
A9,
Th3;
A12: r
<= t by
A10,
XXREAL_0: 30;
A13: p
<= t by
A10,
XXREAL_0: 30;
A14: t
< s by
A11,
XXREAL_0: 23;
A15: t
< q by
A11,
XXREAL_0: 23;
A16: t
in
[.r, s.[ by
A12,
A14,
Th3;
t
in
[.p, q.[ by
A13,
A15,
Th3;
hence thesis by
A16,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:140
(
[.r, s.]
/\
[.p, q.])
=
[.(
max (r,p)), (
min (s,q)).]
proof
let t;
thus t
in (
[.r, s.]
/\
[.p, q.]) implies t
in
[.(
max (r,p)), (
min (s,q)).]
proof
assume
A1: t
in (
[.r, s.]
/\
[.p, q.]);
then
A2: t
in
[.r, s.] by
XBOOLE_0:def 4;
A3: t
in
[.p, q.] by
A1,
XBOOLE_0:def 4;
A4: r
<= t by
A2,
Th1;
A5: t
<= s by
A2,
Th1;
A6: p
<= t by
A3,
Th1;
A7: t
<= q by
A3,
Th1;
A8: (
max (r,p))
<= t by
A4,
A6,
XXREAL_0: 28;
t
<= (
min (s,q)) by
A5,
A7,
XXREAL_0: 20;
hence thesis by
A8,
Th1;
end;
assume
A9: t
in
[.(
max (r,p)), (
min (s,q)).];
then
A10: (
max (r,p))
<= t by
Th1;
A11: t
<= (
min (s,q)) by
A9,
Th1;
A12: r
<= t by
A10,
XXREAL_0: 30;
A13: p
<= t by
A10,
XXREAL_0: 30;
A14: t
<= s by
A11,
XXREAL_0: 22;
A15: t
<= q by
A11,
XXREAL_0: 22;
A16: t
in
[.r, s.] by
A12,
A14,
Th1;
t
in
[.p, q.] by
A13,
A15,
Th1;
hence thesis by
A16,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:141
(
].r, s.]
/\
].p, q.])
=
].(
max (r,p)), (
min (s,q)).]
proof
let t;
thus t
in (
].r, s.]
/\
].p, q.]) implies t
in
].(
max (r,p)), (
min (s,q)).]
proof
assume
A1: t
in (
].r, s.]
/\
].p, q.]);
then
A2: t
in
].r, s.] by
XBOOLE_0:def 4;
A3: t
in
].p, q.] by
A1,
XBOOLE_0:def 4;
A4: r
< t by
A2,
Th2;
A5: t
<= s by
A2,
Th2;
A6: p
< t by
A3,
Th2;
A7: t
<= q by
A3,
Th2;
A8: (
max (r,p))
< t by
A4,
A6,
XXREAL_0: 29;
t
<= (
min (s,q)) by
A5,
A7,
XXREAL_0: 20;
hence thesis by
A8,
Th2;
end;
assume
A9: t
in
].(
max (r,p)), (
min (s,q)).];
then
A10: (
max (r,p))
< t by
Th2;
A11: t
<= (
min (s,q)) by
A9,
Th2;
A12: r
< t by
A10,
XXREAL_0: 31;
A13: p
< t by
A10,
XXREAL_0: 31;
A14: t
<= s by
A11,
XXREAL_0: 22;
A15: t
<= q by
A11,
XXREAL_0: 22;
A16: t
in
].r, s.] by
A12,
A14,
Th2;
t
in
].p, q.] by
A13,
A15,
Th2;
hence thesis by
A16,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:142
(
].r, s.[
/\
].p, q.[)
=
].(
max (r,p)), (
min (s,q)).[
proof
let t;
thus t
in (
].r, s.[
/\
].p, q.[) implies t
in
].(
max (r,p)), (
min (s,q)).[
proof
assume
A1: t
in (
].r, s.[
/\
].p, q.[);
then
A2: t
in
].r, s.[ by
XBOOLE_0:def 4;
A3: t
in
].p, q.[ by
A1,
XBOOLE_0:def 4;
A4: r
< t by
A2,
Th4;
A5: t
< s by
A2,
Th4;
A6: p
< t by
A3,
Th4;
A7: t
< q by
A3,
Th4;
A8: (
max (r,p))
< t by
A4,
A6,
XXREAL_0: 29;
t
< (
min (s,q)) by
A5,
A7,
XXREAL_0: 21;
hence thesis by
A8,
Th4;
end;
assume
A9: t
in
].(
max (r,p)), (
min (s,q)).[;
then
A10: (
max (r,p))
< t by
Th4;
A11: t
< (
min (s,q)) by
A9,
Th4;
A12: r
< t by
A10,
XXREAL_0: 31;
A13: p
< t by
A10,
XXREAL_0: 31;
A14: t
< s by
A11,
XXREAL_0: 23;
A15: t
< q by
A11,
XXREAL_0: 23;
A16: t
in
].r, s.[ by
A12,
A14,
Th4;
t
in
].p, q.[ by
A13,
A15,
Th4;
hence thesis by
A16,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:143
r
<= p & s
<= q implies (
[.r, s.]
/\
[.p, q.])
=
[.p, s.]
proof
assume that
A1: r
<= p and
A2: s
<= q;
let t;
thus t
in (
[.r, s.]
/\
[.p, q.]) implies t
in
[.p, s.]
proof
assume
A3: t
in (
[.r, s.]
/\
[.p, q.]);
then
A4: t
in
[.r, s.] by
XBOOLE_0:def 4;
A5: t
in
[.p, q.] by
A3,
XBOOLE_0:def 4;
A6: t
<= s by
A4,
Th1;
p
<= t by
A5,
Th1;
hence thesis by
A6,
Th1;
end;
assume
A7: t
in
[.p, s.];
then
A8: p
<= t by
Th1;
A9: t
<= s by
A7,
Th1;
A10: r
<= t by
A1,
A8,
XXREAL_0: 2;
A11: t
<= q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
[.r, s.] by
A9,
A10,
Th1;
t
in
[.p, q.] by
A8,
A11,
Th1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:144
r
<= p & s
<= q implies (
[.r, s.[
/\
[.p, q.])
=
[.p, s.[
proof
assume that
A1: r
<= p and
A2: s
<= q;
let t;
thus t
in (
[.r, s.[
/\
[.p, q.]) implies t
in
[.p, s.[
proof
assume
A3: t
in (
[.r, s.[
/\
[.p, q.]);
then
A4: t
in
[.r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.] by
A3,
XBOOLE_0:def 4;
A6: t
< s by
A4,
Th3;
p
<= t by
A5,
Th1;
hence thesis by
A6,
Th3;
end;
assume
A7: t
in
[.p, s.[;
then
A8: p
<= t by
Th3;
A9: t
< s by
A7,
Th3;
A10: r
<= t by
A1,
A8,
XXREAL_0: 2;
A11: t
<= q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
[.r, s.[ by
A9,
A10,
Th3;
t
in
[.p, q.] by
A8,
A11,
Th1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:145
r
>= p & s
> q implies (
[.r, s.[
/\
[.p, q.])
=
[.r, q.]
proof
assume that
A1: r
>= p and
A2: s
> q;
let t;
thus t
in (
[.r, s.[
/\
[.p, q.]) implies t
in
[.r, q.]
proof
assume
A3: t
in (
[.r, s.[
/\
[.p, q.]);
then
A4: t
in
[.r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.] by
A3,
XBOOLE_0:def 4;
A6: r
<= t by
A4,
Th3;
t
<= q by
A5,
Th1;
hence thesis by
A6,
Th1;
end;
assume
A7: t
in
[.r, q.];
then
A8: r
<= t by
Th1;
A9: t
<= q by
A7,
Th1;
then
A10: t
< s by
A2,
XXREAL_0: 2;
A11: p
<= t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
[.r, s.[ by
A8,
A10,
Th3;
t
in
[.p, q.] by
A9,
A11,
Th1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:146
r
< p & s
<= q implies (
].r, s.]
/\
[.p, q.])
=
[.p, s.]
proof
assume that
A1: r
< p and
A2: s
<= q;
let t;
thus t
in (
].r, s.]
/\
[.p, q.]) implies t
in
[.p, s.]
proof
assume
A3: t
in (
].r, s.]
/\
[.p, q.]);
then
A4: t
in
].r, s.] by
XBOOLE_0:def 4;
A5: t
in
[.p, q.] by
A3,
XBOOLE_0:def 4;
A6: t
<= s by
A4,
Th2;
p
<= t by
A5,
Th1;
hence thesis by
A6,
Th1;
end;
assume
A7: t
in
[.p, s.];
then
A8: p
<= t by
Th1;
A9: t
<= s by
A7,
Th1;
A10: r
< t by
A1,
A8,
XXREAL_0: 2;
A11: t
<= q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
].r, s.] by
A9,
A10,
Th2;
t
in
[.p, q.] by
A8,
A11,
Th1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:147
r
>= p & s
>= q implies (
].r, s.]
/\
[.p, q.])
=
].r, q.]
proof
assume that
A1: r
>= p and
A2: s
>= q;
let t;
thus t
in (
].r, s.]
/\
[.p, q.]) implies t
in
].r, q.]
proof
assume
A3: t
in (
].r, s.]
/\
[.p, q.]);
then
A4: t
in
].r, s.] by
XBOOLE_0:def 4;
A5: t
in
[.p, q.] by
A3,
XBOOLE_0:def 4;
A6: r
< t by
A4,
Th2;
t
<= q by
A5,
Th1;
hence thesis by
A6,
Th2;
end;
assume
A7: t
in
].r, q.];
then
A8: r
< t by
Th2;
A9: t
<= q by
A7,
Th2;
then
A10: t
<= s by
A2,
XXREAL_0: 2;
A11: p
<= t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
].r, s.] by
A8,
A10,
Th2;
t
in
[.p, q.] by
A9,
A11,
Th1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:148
r
< p & s
<= q implies (
].r, s.[
/\
[.p, q.])
=
[.p, s.[
proof
assume that
A1: r
< p and
A2: s
<= q;
let t;
thus t
in (
].r, s.[
/\
[.p, q.]) implies t
in
[.p, s.[
proof
assume
A3: t
in (
].r, s.[
/\
[.p, q.]);
then
A4: t
in
].r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.] by
A3,
XBOOLE_0:def 4;
A6: t
< s by
A4,
Th4;
p
<= t by
A5,
Th1;
hence thesis by
A6,
Th3;
end;
assume
A7: t
in
[.p, s.[;
then
A8: p
<= t by
Th3;
A9: t
< s by
A7,
Th3;
A10: r
< t by
A1,
A8,
XXREAL_0: 2;
A11: t
<= q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
].r, s.[ by
A9,
A10,
Th4;
t
in
[.p, q.] by
A8,
A11,
Th1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:149
r
>= p & s
> q implies (
].r, s.[
/\
[.p, q.])
=
].r, q.]
proof
assume that
A1: r
>= p and
A2: s
> q;
let t;
thus t
in (
].r, s.[
/\
[.p, q.]) implies t
in
].r, q.]
proof
assume
A3: t
in (
].r, s.[
/\
[.p, q.]);
then
A4: t
in
].r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.] by
A3,
XBOOLE_0:def 4;
A6: r
< t by
A4,
Th4;
t
<= q by
A5,
Th1;
hence thesis by
A6,
Th2;
end;
assume
A7: t
in
].r, q.];
then
A8: r
< t by
Th2;
A9: t
<= q by
A7,
Th2;
then
A10: t
< s by
A2,
XXREAL_0: 2;
A11: p
<= t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
].r, s.[ by
A8,
A10,
Th4;
t
in
[.p, q.] by
A9,
A11,
Th1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:150
r
<= p & s
<= q implies (
[.r, s.[
/\
[.p, q.[)
=
[.p, s.[
proof
assume that
A1: r
<= p and
A2: s
<= q;
let t;
thus t
in (
[.r, s.[
/\
[.p, q.[) implies t
in
[.p, s.[
proof
assume
A3: t
in (
[.r, s.[
/\
[.p, q.[);
then
A4: t
in
[.r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.[ by
A3,
XBOOLE_0:def 4;
A6: t
< s by
A4,
Th3;
p
<= t by
A5,
Th3;
hence thesis by
A6,
Th3;
end;
assume
A7: t
in
[.p, s.[;
then
A8: p
<= t by
Th3;
A9: t
< s by
A7,
Th3;
A10: r
<= t by
A1,
A8,
XXREAL_0: 2;
A11: t
< q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
[.r, s.[ by
A9,
A10,
Th3;
t
in
[.p, q.[ by
A8,
A11,
Th3;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:151
r
>= p & s
>= q implies (
[.r, s.[
/\
[.p, q.[)
=
[.r, q.[
proof
assume that
A1: r
>= p and
A2: s
>= q;
let t;
thus t
in (
[.r, s.[
/\
[.p, q.[) implies t
in
[.r, q.[
proof
assume
A3: t
in (
[.r, s.[
/\
[.p, q.[);
then
A4: t
in
[.r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.[ by
A3,
XBOOLE_0:def 4;
A6: r
<= t by
A4,
Th3;
t
< q by
A5,
Th3;
hence thesis by
A6,
Th3;
end;
assume
A7: t
in
[.r, q.[;
then
A8: r
<= t by
Th3;
A9: t
< q by
A7,
Th3;
then
A10: t
< s by
A2,
XXREAL_0: 2;
A11: p
<= t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
[.r, s.[ by
A8,
A10,
Th3;
t
in
[.p, q.[ by
A9,
A11,
Th3;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:152
Th152: r
< p & s
< q implies (
].r, s.]
/\
[.p, q.[)
=
[.p, s.]
proof
assume that
A1: r
< p and
A2: s
< q;
let t;
thus t
in (
].r, s.]
/\
[.p, q.[) implies t
in
[.p, s.]
proof
assume
A3: t
in (
].r, s.]
/\
[.p, q.[);
then
A4: t
in
].r, s.] by
XBOOLE_0:def 4;
A5: t
in
[.p, q.[ by
A3,
XBOOLE_0:def 4;
A6: t
<= s by
A4,
Th2;
p
<= t by
A5,
Th3;
hence thesis by
A6,
Th1;
end;
assume
A7: t
in
[.p, s.];
then
A8: p
<= t by
Th1;
A9: t
<= s by
A7,
Th1;
A10: r
< t by
A1,
A8,
XXREAL_0: 2;
A11: t
< q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
].r, s.] by
A9,
A10,
Th2;
t
in
[.p, q.[ by
A8,
A11,
Th3;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:153
r
>= p & s
>= q implies (
].r, s.]
/\
[.p, q.[)
=
].r, q.[
proof
assume that
A1: r
>= p and
A2: s
>= q;
let t;
thus t
in (
].r, s.]
/\
[.p, q.[) implies t
in
].r, q.[
proof
assume
A3: t
in (
].r, s.]
/\
[.p, q.[);
then
A4: t
in
].r, s.] by
XBOOLE_0:def 4;
A5: t
in
[.p, q.[ by
A3,
XBOOLE_0:def 4;
A6: r
< t by
A4,
Th2;
t
< q by
A5,
Th3;
hence thesis by
A6,
Th4;
end;
assume
A7: t
in
].r, q.[;
then
A8: r
< t by
Th4;
A9: t
< q by
A7,
Th4;
then
A10: t
<= s by
A2,
XXREAL_0: 2;
A11: p
<= t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
].r, s.] by
A8,
A10,
Th2;
t
in
[.p, q.[ by
A9,
A11,
Th3;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:154
Th154: r
< p & s
<= q implies (
].r, s.[
/\
[.p, q.[)
=
[.p, s.[
proof
assume that
A1: r
< p and
A2: s
<= q;
let t;
thus t
in (
].r, s.[
/\
[.p, q.[) implies t
in
[.p, s.[
proof
assume
A3: t
in (
].r, s.[
/\
[.p, q.[);
then
A4: t
in
].r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.[ by
A3,
XBOOLE_0:def 4;
A6: t
< s by
A4,
Th4;
p
<= t by
A5,
Th3;
hence thesis by
A6,
Th3;
end;
assume
A7: t
in
[.p, s.[;
then
A8: p
<= t by
Th3;
A9: t
< s by
A7,
Th3;
A10: r
< t by
A1,
A8,
XXREAL_0: 2;
A11: t
< q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
].r, s.[ by
A9,
A10,
Th4;
t
in
[.p, q.[ by
A8,
A11,
Th3;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:155
r
>= p & s
>= q implies (
].r, s.[
/\
[.p, q.[)
=
].r, q.[
proof
assume that
A1: r
>= p and
A2: s
>= q;
let t;
thus t
in (
].r, s.[
/\
[.p, q.[) implies t
in
].r, q.[
proof
assume
A3: t
in (
].r, s.[
/\
[.p, q.[);
then
A4: t
in
].r, s.[ by
XBOOLE_0:def 4;
A5: t
in
[.p, q.[ by
A3,
XBOOLE_0:def 4;
A6: r
< t by
A4,
Th4;
t
< q by
A5,
Th3;
hence thesis by
A6,
Th4;
end;
assume
A7: t
in
].r, q.[;
then
A8: r
< t by
Th4;
A9: t
< q by
A7,
Th4;
then
A10: t
< s by
A2,
XXREAL_0: 2;
A11: p
<= t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
].r, s.[ by
A8,
A10,
Th4;
t
in
[.p, q.[ by
A9,
A11,
Th3;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:156
r
<= p & s
<= q implies (
].r, s.]
/\
].p, q.])
=
].p, s.]
proof
assume that
A1: r
<= p and
A2: s
<= q;
let t;
thus t
in (
].r, s.]
/\
].p, q.]) implies t
in
].p, s.]
proof
assume
A3: t
in (
].r, s.]
/\
].p, q.]);
then
A4: t
in
].r, s.] by
XBOOLE_0:def 4;
A5: t
in
].p, q.] by
A3,
XBOOLE_0:def 4;
A6: t
<= s by
A4,
Th2;
p
< t by
A5,
Th2;
hence thesis by
A6,
Th2;
end;
assume
A7: t
in
].p, s.];
then
A8: p
< t by
Th2;
A9: t
<= s by
A7,
Th2;
A10: r
< t by
A1,
A8,
XXREAL_0: 2;
A11: t
<= q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
].r, s.] by
A9,
A10,
Th2;
t
in
].p, q.] by
A8,
A11,
Th2;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:157
r
>= p & s
>= q implies (
].r, s.]
/\
].p, q.])
=
].r, q.]
proof
assume that
A1: r
>= p and
A2: s
>= q;
let t;
thus t
in (
].r, s.]
/\
].p, q.]) implies t
in
].r, q.]
proof
assume
A3: t
in (
].r, s.]
/\
].p, q.]);
then
A4: t
in
].r, s.] by
XBOOLE_0:def 4;
A5: t
in
].p, q.] by
A3,
XBOOLE_0:def 4;
A6: r
< t by
A4,
Th2;
t
<= q by
A5,
Th2;
hence thesis by
A6,
Th2;
end;
assume
A7: t
in
].r, q.];
then
A8: r
< t by
Th2;
A9: t
<= q by
A7,
Th2;
then
A10: t
<= s by
A2,
XXREAL_0: 2;
A11: p
< t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
].r, s.] by
A8,
A10,
Th2;
t
in
].p, q.] by
A9,
A11,
Th2;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:158
r
<= p & s
<= q implies (
].r, s.[
/\
].p, q.])
=
].p, s.[
proof
assume that
A1: r
<= p and
A2: s
<= q;
let t;
thus t
in (
].r, s.[
/\
].p, q.]) implies t
in
].p, s.[
proof
assume
A3: t
in (
].r, s.[
/\
].p, q.]);
then
A4: t
in
].r, s.[ by
XBOOLE_0:def 4;
A5: t
in
].p, q.] by
A3,
XBOOLE_0:def 4;
A6: t
< s by
A4,
Th4;
p
< t by
A5,
Th2;
hence thesis by
A6,
Th4;
end;
assume
A7: t
in
].p, s.[;
then
A8: p
< t by
Th4;
A9: t
< s by
A7,
Th4;
A10: r
< t by
A1,
A8,
XXREAL_0: 2;
A11: t
<= q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
].r, s.[ by
A9,
A10,
Th4;
t
in
].p, q.] by
A8,
A11,
Th2;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:159
Th159: r
>= p & s
> q implies (
].r, s.[
/\
].p, q.])
=
].r, q.]
proof
assume that
A1: r
>= p and
A2: s
> q;
let t;
thus t
in (
].r, s.[
/\
].p, q.]) implies t
in
].r, q.]
proof
assume
A3: t
in (
].r, s.[
/\
].p, q.]);
then
A4: t
in
].r, s.[ by
XBOOLE_0:def 4;
A5: t
in
].p, q.] by
A3,
XBOOLE_0:def 4;
A6: r
< t by
A4,
Th4;
t
<= q by
A5,
Th2;
hence thesis by
A6,
Th2;
end;
assume
A7: t
in
].r, q.];
then
A8: r
< t by
Th2;
A9: t
<= q by
A7,
Th2;
then
A10: t
< s by
A2,
XXREAL_0: 2;
A11: p
< t by
A1,
A8,
XXREAL_0: 2;
A12: t
in
].r, s.[ by
A8,
A10,
Th4;
t
in
].p, q.] by
A9,
A11,
Th2;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:160
Th160: r
<= p & s
<= q implies (
].r, s.[
/\
].p, q.[)
=
].p, s.[
proof
assume that
A1: r
<= p and
A2: s
<= q;
let t;
thus t
in (
].r, s.[
/\
].p, q.[) implies t
in
].p, s.[
proof
assume
A3: t
in (
].r, s.[
/\
].p, q.[);
then
A4: t
in
].r, s.[ by
XBOOLE_0:def 4;
A5: t
in
].p, q.[ by
A3,
XBOOLE_0:def 4;
A6: t
< s by
A4,
Th4;
p
< t by
A5,
Th4;
hence thesis by
A6,
Th4;
end;
assume
A7: t
in
].p, s.[;
then
A8: p
< t by
Th4;
A9: t
< s by
A7,
Th4;
A10: r
< t by
A1,
A8,
XXREAL_0: 2;
A11: t
< q by
A2,
A9,
XXREAL_0: 2;
A12: t
in
].r, s.[ by
A9,
A10,
Th4;
t
in
].p, q.[ by
A8,
A11,
Th4;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
theorem ::
XXREAL_1:161
(
[.r, s.[
\/
[.p, q.[)
c=
[.(
min (r,p)), (
max (s,q)).[
proof
let t;
assume t
in (
[.r, s.[
\/
[.p, q.[);
then t
in
[.r, s.[ or t
in
[.p, q.[ by
XBOOLE_0:def 3;
then
A1: r
<= t & t
< s or p
<= t & t
< q by
Th3;
then
A2: (
min (r,p))
<= t by
XXREAL_0: 23;
t
< (
max (s,q)) by
A1,
XXREAL_0: 30;
hence thesis by
A2,
Th3;
end;
theorem ::
XXREAL_1:162
[.r, s.[
meets
[.p, q.[ implies (
[.r, s.[
\/
[.p, q.[)
=
[.(
min (r,p)), (
max (s,q)).[
proof
assume
[.r, s.[
meets
[.p, q.[;
then
consider u such that
A1: u
in
[.r, s.[ and
A2: u
in
[.p, q.[;
let t;
thus t
in (
[.r, s.[
\/
[.p, q.[) implies t
in
[.(
min (r,p)), (
max (s,q)).[
proof
assume t
in (
[.r, s.[
\/
[.p, q.[);
then t
in
[.r, s.[ or t
in
[.p, q.[ by
XBOOLE_0:def 3;
then
A3: r
<= t & t
< s or p
<= t & t
< q by
Th3;
then
A4: (
min (r,p))
<= t by
XXREAL_0: 23;
t
< (
max (s,q)) by
A3,
XXREAL_0: 30;
hence thesis by
A4,
Th3;
end;
A5: r
<= u by
A1,
Th3;
A6: u
< s by
A1,
Th3;
A7: p
<= u by
A2,
Th3;
A8: u
< q by
A2,
Th3;
assume
A9: t
in
[.(
min (r,p)), (
max (s,q)).[;
then
A10: (
min (r,p))
<= t by
Th3;
A11: t
< (
max (s,q)) by
A9,
Th3;
per cases by
A10,
A11,
XXREAL_0: 21,
XXREAL_0: 28;
suppose r
<= t & t
< s or p
<= t & t
< q;
then t
in
[.r, s.[ or t
in
[.p, q.[ by
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
suppose that
A12: p
<= t and
A13: t
< s;
u
<= t or t
<= u;
then r
<= t or t
< q by
A5,
A8,
XXREAL_0: 2;
then t
in
[.r, s.[ or t
in
[.p, q.[ by
A12,
A13,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
suppose that
A14: r
<= t and
A15: t
< q;
u
<= t or t
<= u;
then t
< s or p
<= t by
A6,
A7,
XXREAL_0: 2;
then t
in
[.r, s.[ or t
in
[.p, q.[ by
A14,
A15,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
end;
theorem ::
XXREAL_1:163
(
].r, s.]
\/
].p, q.])
c=
].(
min (r,p)), (
max (s,q)).]
proof
let t;
assume t
in (
].r, s.]
\/
].p, q.]);
then t
in
].r, s.] or t
in
].p, q.] by
XBOOLE_0:def 3;
then
A1: r
< t & t
<= s or p
< t & t
<= q by
Th2;
then
A2: (
min (r,p))
< t by
XXREAL_0: 22;
t
<= (
max (s,q)) by
A1,
XXREAL_0: 31;
hence thesis by
A2,
Th2;
end;
theorem ::
XXREAL_1:164
].r, s.]
meets
].p, q.] implies (
].r, s.]
\/
].p, q.])
=
].(
min (r,p)), (
max (s,q)).]
proof
assume
].r, s.]
meets
].p, q.];
then
consider u such that
A1: u
in
].r, s.] and
A2: u
in
].p, q.];
let t;
thus t
in (
].r, s.]
\/
].p, q.]) implies t
in
].(
min (r,p)), (
max (s,q)).]
proof
assume t
in (
].r, s.]
\/
].p, q.]);
then t
in
].r, s.] or t
in
].p, q.] by
XBOOLE_0:def 3;
then
A3: r
< t & t
<= s or p
< t & t
<= q by
Th2;
then
A4: (
min (r,p))
< t by
XXREAL_0: 22;
t
<= (
max (s,q)) by
A3,
XXREAL_0: 31;
hence thesis by
A4,
Th2;
end;
A5: r
< u by
A1,
Th2;
A6: u
<= s by
A1,
Th2;
A7: p
< u by
A2,
Th2;
A8: u
<= q by
A2,
Th2;
assume
A9: t
in
].(
min (r,p)), (
max (s,q)).];
then
A10: (
min (r,p))
< t by
Th2;
A11: t
<= (
max (s,q)) by
A9,
Th2;
per cases by
A10,
A11,
XXREAL_0: 20,
XXREAL_0: 29;
suppose r
< t & t
<= s or p
< t & t
<= q;
then t
in
].r, s.] or t
in
].p, q.] by
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
suppose that
A12: p
< t and
A13: t
<= s;
u
<= t or t
<= u;
then r
< t or t
<= q by
A5,
A8,
XXREAL_0: 2;
then t
in
].r, s.] or t
in
].p, q.] by
A12,
A13,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
suppose that
A14: r
< t and
A15: t
<= q;
u
<= t or t
<= u;
then t
<= s or p
< t by
A6,
A7,
XXREAL_0: 2;
then t
in
].r, s.] or t
in
].p, q.] by
A14,
A15,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
end;
theorem ::
XXREAL_1:165
r
<= s & s
<= t implies (
[.r, s.]
\/
[.s, t.])
=
[.r, t.]
proof
assume that
A1: r
<= s and
A2: s
<= t;
let p;
thus p
in (
[.r, s.]
\/
[.s, t.]) implies p
in
[.r, t.]
proof
assume p
in (
[.r, s.]
\/
[.s, t.]);
then p
in
[.r, s.] or p
in
[.s, t.] by
XBOOLE_0:def 3;
then
A3: r
<= p & p
<= s or s
<= p & p
<= t by
Th1;
then
A4: r
<= p by
A1,
XXREAL_0: 2;
p
<= t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th1;
end;
assume p
in
[.r, t.];
then r
<= p & p
<= s or s
<= p & p
<= t by
Th1;
then p
in
[.r, s.] or p
in
[.s, t.] by
Th1;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:166
Th166: r
<= s & s
<= t implies (
[.r, s.[
\/
[.s, t.])
=
[.r, t.]
proof
assume that
A1: r
<= s and
A2: s
<= t;
let p;
thus p
in (
[.r, s.[
\/
[.s, t.]) implies p
in
[.r, t.]
proof
assume p
in (
[.r, s.[
\/
[.s, t.]);
then p
in
[.r, s.[ or p
in
[.s, t.] by
XBOOLE_0:def 3;
then
A3: r
<= p & p
< s or s
<= p & p
<= t by
Th1,
Th3;
then
A4: r
<= p by
A1,
XXREAL_0: 2;
p
<= t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th1;
end;
assume p
in
[.r, t.];
then r
<= p & p
< s or s
<= p & p
<= t by
Th1;
then p
in
[.r, s.[ or p
in
[.s, t.] by
Th1,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:167
Th167: r
<= s & s
<= t implies (
[.r, s.]
\/
].s, t.])
=
[.r, t.]
proof
assume that
A1: r
<= s and
A2: s
<= t;
let p;
thus p
in (
[.r, s.]
\/
].s, t.]) implies p
in
[.r, t.]
proof
assume p
in (
[.r, s.]
\/
].s, t.]);
then p
in
[.r, s.] or p
in
].s, t.] by
XBOOLE_0:def 3;
then
A3: r
<= p & p
<= s or s
< p & p
<= t by
Th1,
Th2;
then
A4: r
<= p by
A1,
XXREAL_0: 2;
p
<= t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th1;
end;
assume p
in
[.r, t.];
then r
<= p & p
<= s or s
< p & p
<= t by
Th1;
then p
in
[.r, s.] or p
in
].s, t.] by
Th1,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:168
r
<= s & s
<= t implies (
[.r, s.[
\/
[.s, t.[)
=
[.r, t.[
proof
assume that
A1: r
<= s and
A2: s
<= t;
let p;
thus p
in (
[.r, s.[
\/
[.s, t.[) implies p
in
[.r, t.[
proof
assume p
in (
[.r, s.[
\/
[.s, t.[);
then p
in
[.r, s.[ or p
in
[.s, t.[ by
XBOOLE_0:def 3;
then
A3: r
<= p & p
< s or s
<= p & p
< t by
Th3;
then
A4: r
<= p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th3;
end;
assume p
in
[.r, t.[;
then r
<= p & p
< s or s
<= p & p
< t by
Th3;
then p
in
[.r, s.[ or p
in
[.s, t.[ by
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:169
Th169: r
<= s & s
< t implies (
[.r, s.]
\/
].s, t.[)
=
[.r, t.[
proof
assume that
A1: r
<= s and
A2: s
< t;
let p;
thus p
in (
[.r, s.]
\/
].s, t.[) implies p
in
[.r, t.[
proof
assume p
in (
[.r, s.]
\/
].s, t.[);
then p
in
[.r, s.] or p
in
].s, t.[ by
XBOOLE_0:def 3;
then
A3: r
<= p & p
<= s or s
< p & p
< t by
Th1,
Th4;
then
A4: r
<= p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th3;
end;
assume p
in
[.r, t.[;
then r
<= p & p
<= s or s
< p & p
< t by
Th3;
then p
in
[.r, s.] or p
in
].s, t.[ by
Th1,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:170
r
<= s & s
<= t implies (
].r, s.]
\/
].s, t.])
=
].r, t.]
proof
assume that
A1: r
<= s and
A2: s
<= t;
let p;
thus p
in (
].r, s.]
\/
].s, t.]) implies p
in
].r, t.]
proof
assume p
in (
].r, s.]
\/
].s, t.]);
then p
in
].r, s.] or p
in
].s, t.] by
XBOOLE_0:def 3;
then
A3: r
< p & p
<= s or s
< p & p
<= t by
Th2;
then
A4: r
< p by
A1,
XXREAL_0: 2;
p
<= t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th2;
end;
assume p
in
].r, t.];
then r
< p & p
<= s or s
< p & p
<= t by
Th2;
then p
in
].r, s.] or p
in
].s, t.] by
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:171
Th171: r
<= s & s
< t implies (
].r, s.]
\/
].s, t.[)
=
].r, t.[
proof
assume that
A1: r
<= s and
A2: s
< t;
let p;
thus p
in (
].r, s.]
\/
].s, t.[) implies p
in
].r, t.[
proof
assume p
in (
].r, s.]
\/
].s, t.[);
then p
in
].r, s.] or p
in
].s, t.[ by
XBOOLE_0:def 3;
then
A3: r
< p & p
<= s or s
< p & p
< t by
Th2,
Th4;
then
A4: r
< p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th4;
end;
assume p
in
].r, t.[;
then r
< p & p
<= s or s
< p & p
< t by
Th4;
then p
in
].r, s.] or p
in
].s, t.[ by
Th2,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:172
r
< s & s
< t implies (
].r, s.]
\/
[.s, t.[)
=
].r, t.[
proof
assume that
A1: r
< s and
A2: s
< t;
let p;
thus p
in (
].r, s.]
\/
[.s, t.[) implies p
in
].r, t.[
proof
assume p
in (
].r, s.]
\/
[.s, t.[);
then p
in
].r, s.] or p
in
[.s, t.[ by
XBOOLE_0:def 3;
then
A3: r
< p & p
<= s or s
<= p & p
< t by
Th2,
Th3;
then
A4: r
< p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th4;
end;
assume p
in
].r, t.[;
then r
< p & p
<= s or s
< p & p
< t by
Th4;
then p
in
].r, s.] or p
in
[.s, t.[ by
Th2,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:173
Th173: r
< s & s
< t implies (
].r, s.[
\/
[.s, t.[)
=
].r, t.[
proof
assume that
A1: r
< s and
A2: s
< t;
let p;
thus p
in (
].r, s.[
\/
[.s, t.[) implies p
in
].r, t.[
proof
assume p
in (
].r, s.[
\/
[.s, t.[);
then p
in
].r, s.[ or p
in
[.s, t.[ by
XBOOLE_0:def 3;
then
A3: r
< p & p
< s or s
<= p & p
< t by
Th3,
Th4;
then
A4: r
< p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th4;
end;
assume p
in
].r, t.[;
then r
< p & p
< s or s
<= p & p
< t by
Th4;
then p
in
].r, s.[ or p
in
[.s, t.[ by
Th3,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:174
Th174: p
<= s & r
<= q & s
<= r implies (
[.p, r.]
\/
[.s, q.])
=
[.p, q.]
proof
assume that
A1: p
<= s and
A2: r
<= q and
A3: s
<= r;
let t;
thus t
in (
[.p, r.]
\/
[.s, q.]) implies t
in
[.p, q.]
proof
assume t
in (
[.p, r.]
\/
[.s, q.]);
then t
in
[.p, r.] or t
in
[.s, q.] by
XBOOLE_0:def 3;
then
A4: p
<= t & t
<= r or s
<= t & t
<= q by
Th1;
then
A5: p
<= t by
A1,
XXREAL_0: 2;
t
<= q by
A2,
A4,
XXREAL_0: 2;
hence thesis by
A5,
Th1;
end;
assume t
in
[.p, q.];
then p
<= t & t
<= r or s
<= t & t
<= q by
A3,
Th1,
XXREAL_0: 2;
then t
in
[.p, r.] or t
in
[.s, q.] by
Th1;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:175
Th175: p
<= s & r
<= q & s
< r implies (
[.p, r.[
\/
].s, q.])
=
[.p, q.]
proof
assume that
A1: p
<= s and
A2: r
<= q and
A3: s
< r;
let t;
thus t
in (
[.p, r.[
\/
].s, q.]) implies t
in
[.p, q.]
proof
assume t
in (
[.p, r.[
\/
].s, q.]);
then t
in
[.p, r.[ or t
in
].s, q.] by
XBOOLE_0:def 3;
then
A4: p
<= t & t
<= r or s
<= t & t
<= q by
Th2,
Th3;
then
A5: p
<= t by
A1,
XXREAL_0: 2;
t
<= q by
A2,
A4,
XXREAL_0: 2;
hence thesis by
A5,
Th1;
end;
assume t
in
[.p, q.];
then p
<= t & t
< r or s
< t & t
<= q by
A3,
Th1,
XXREAL_0: 2;
then t
in
[.p, r.[ or t
in
].s, q.] by
Th2,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:176
p
<= s & s
<= r & r
< q implies (
[.p, r.]
\/
[.s, q.[)
=
[.p, q.[
proof
assume that
A1: p
<= s and
A2: s
<= r and
A3: r
< q;
let t;
thus t
in (
[.p, r.]
\/
[.s, q.[) implies t
in
[.p, q.[
proof
assume t
in (
[.p, r.]
\/
[.s, q.[);
then t
in
[.p, r.] or t
in
[.s, q.[ by
XBOOLE_0:def 3;
then
A4: p
<= t & t
<= r or s
<= t & t
< q by
Th1,
Th3;
then
A5: p
<= t by
A1,
XXREAL_0: 2;
t
< q by
A3,
A4,
XXREAL_0: 2;
hence thesis by
A5,
Th3;
end;
assume t
in
[.p, q.[;
then p
<= t & t
<= r or s
<= t & t
< q by
A2,
Th3,
XXREAL_0: 2;
then t
in
[.p, r.] or t
in
[.s, q.[ by
Th1,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:177
p
< s & r
<= q & s
<= r implies (
].p, r.]
\/
[.s, q.])
=
].p, q.]
proof
assume that
A1: p
< s and
A2: r
<= q and
A3: s
<= r;
let t;
thus t
in (
].p, r.]
\/
[.s, q.]) implies t
in
].p, q.]
proof
assume t
in (
].p, r.]
\/
[.s, q.]);
then t
in
].p, r.] or t
in
[.s, q.] by
XBOOLE_0:def 3;
then
A4: p
< t & t
<= r or s
<= t & t
<= q by
Th1,
Th2;
then
A5: p
< t by
A1,
XXREAL_0: 2;
t
<= q by
A2,
A4,
XXREAL_0: 2;
hence thesis by
A5,
Th2;
end;
assume t
in
].p, q.];
then p
< t & t
<= r or s
<= t & t
<= q by
A3,
Th2,
XXREAL_0: 2;
then t
in
].p, r.] or t
in
[.s, q.] by
Th1,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:178
Th178: p
< s & r
< q & s
<= r implies (
].p, r.]
\/
[.s, q.[)
=
].p, q.[
proof
assume that
A1: p
< s and
A2: r
< q and
A3: s
<= r;
let t;
thus t
in (
].p, r.]
\/
[.s, q.[) implies t
in
].p, q.[
proof
assume t
in (
].p, r.]
\/
[.s, q.[);
then t
in
].p, r.] or t
in
[.s, q.[ by
XBOOLE_0:def 3;
then
A4: p
< t & t
<= r or s
<= t & t
< q by
Th2,
Th3;
then
A5: p
< t by
A1,
XXREAL_0: 2;
t
< q by
A2,
A4,
XXREAL_0: 2;
hence thesis by
A5,
Th4;
end;
assume t
in
].p, q.[;
then p
< t & t
<= r or s
<= t & t
< q by
A3,
Th4,
XXREAL_0: 2;
then t
in
].p, r.] or t
in
[.s, q.[ by
Th2,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:179
p
<= r & p
<= s & r
<= q & s
<= q implies ((
[.p, r.[
\/
[.r, s.])
\/
].s, q.])
=
[.p, q.]
proof
assume that
A1: p
<= r and
A2: p
<= s and
A3: r
<= q and
A4: s
<= q;
per cases ;
suppose r
<= s;
hence ((
[.p, r.[
\/
[.r, s.])
\/
].s, q.])
= (
[.p, s.]
\/
].s, q.]) by
A1,
Th166
.=
[.p, q.] by
A2,
A4,
Th167;
end;
suppose
A5: s
< r;
hence ((
[.p, r.[
\/
[.r, s.])
\/
].s, q.])
= ((
[.p, r.[
\/
{} )
\/
].s, q.]) by
Th29
.=
[.p, q.] by
A2,
A3,
A5,
Th175;
end;
end;
theorem ::
XXREAL_1:180
p
< r & p
< s & r
< q & s
< q implies ((
].p, r.]
\/
].r, s.[)
\/
[.s, q.[)
=
].p, q.[
proof
assume that
A1: p
< r and
A2: p
< s and
A3: r
< q and
A4: s
< q;
per cases ;
suppose r
< s;
hence ((
].p, r.]
\/
].r, s.[)
\/
[.s, q.[)
= (
].p, s.[
\/
[.s, q.[) by
A1,
Th171
.=
].p, q.[ by
A2,
A4,
Th173;
end;
suppose
A5: s
<= r;
hence ((
].p, r.]
\/
].r, s.[)
\/
[.s, q.[)
= ((
].p, r.]
\/
{} )
\/
[.s, q.[) by
Th28
.=
].p, q.[ by
A2,
A3,
A5,
Th178;
end;
end;
theorem ::
XXREAL_1:181
p
<= r & r
<= s & s
<= q implies ((
[.p, r.]
\/
].r, s.[)
\/
[.s, q.])
=
[.p, q.]
proof
assume that
A1: p
<= r and
A2: r
<= s and
A3: s
<= q;
A4: p
<= s by
A1,
A2,
XXREAL_0: 2;
A5: r
<= q by
A2,
A3,
XXREAL_0: 2;
per cases ;
suppose r
< s;
hence ((
[.p, r.]
\/
].r, s.[)
\/
[.s, q.])
= (
[.p, s.[
\/
[.s, q.]) by
A1,
Th169
.=
[.p, q.] by
A3,
A4,
Th166;
end;
suppose
A6: s
<= r;
hence ((
[.p, r.]
\/
].r, s.[)
\/
[.s, q.])
= ((
[.p, r.]
\/
{} )
\/
[.s, q.]) by
Th28
.=
[.p, q.] by
A4,
A5,
A6,
Th174;
end;
end;
theorem ::
XXREAL_1:182
Th182: r
<= s implies (
[.r, t.]
\
[.r, s.])
=
].s, t.]
proof
assume that
A1: r
<= s;
let p;
thus p
in (
[.r, t.]
\
[.r, s.]) implies p
in
].s, t.]
proof
assume
A2: p
in (
[.r, t.]
\
[.r, s.]);
then
A3: not p
in
[.r, s.] by
XBOOLE_0:def 5;
A4: p
<= t by
A2,
Th1;
p
< r or s
< p by
A3,
Th1;
hence thesis by
A2,
A4,
Th1,
Th2;
end;
assume
A5: p
in
].s, t.];
then
A6: s
< p by
Th2;
then
A7: r
<= p by
A1,
XXREAL_0: 2;
p
<= t by
A5,
Th2;
then
A8: p
in
[.r, t.] by
A7,
Th1;
not p
in
[.r, s.] by
A6,
Th1;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:183
Th183: r
<= s implies (
[.r, t.[
\
[.r, s.])
=
].s, t.[
proof
assume that
A1: r
<= s;
let p;
thus p
in (
[.r, t.[
\
[.r, s.]) implies p
in
].s, t.[
proof
assume
A2: p
in (
[.r, t.[
\
[.r, s.]);
then
A3: not p
in
[.r, s.] by
XBOOLE_0:def 5;
A4: p
< t by
A2,
Th3;
p
< r or s
< p by
A3,
Th1;
hence thesis by
A2,
A4,
Th3,
Th4;
end;
assume
A5: p
in
].s, t.[;
then
A6: s
< p by
Th4;
then
A7: r
<= p by
A1,
XXREAL_0: 2;
p
< t by
A5,
Th4;
then
A8: p
in
[.r, t.[ by
A7,
Th3;
not p
in
[.r, s.] by
A6,
Th1;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:184
Th184: r
< s implies (
[.r, t.]
\
[.r, s.[)
=
[.s, t.]
proof
assume that
A1: r
< s;
let p;
thus p
in (
[.r, t.]
\
[.r, s.[) implies p
in
[.s, t.]
proof
assume
A2: p
in (
[.r, t.]
\
[.r, s.[);
then
A3: not p
in
[.r, s.[ by
XBOOLE_0:def 5;
A4: p
<= t by
A2,
Th1;
p
< r or s
<= p by
A3,
Th3;
hence thesis by
A2,
A4,
Th1;
end;
assume
A5: p
in
[.s, t.];
then
A6: s
<= p by
Th1;
then
A7: r
<= p by
A1,
XXREAL_0: 2;
p
<= t by
A5,
Th1;
then
A8: p
in
[.r, t.] by
A7,
Th1;
not p
in
[.r, s.[ by
A6,
Th3;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:185
Th185: r
< s implies (
[.r, t.[
\
[.r, s.[)
=
[.s, t.[
proof
assume that
A1: r
< s;
let p;
thus p
in (
[.r, t.[
\
[.r, s.[) implies p
in
[.s, t.[
proof
assume
A2: p
in (
[.r, t.[
\
[.r, s.[);
then
A3: not p
in
[.r, s.[ by
XBOOLE_0:def 5;
A4: p
< t by
A2,
Th3;
p
< r or s
<= p by
A3,
Th3;
hence thesis by
A2,
A4,
Th3;
end;
assume
A5: p
in
[.s, t.[;
then
A6: s
<= p by
Th3;
then
A7: r
<= p by
A1,
XXREAL_0: 2;
p
< t by
A5,
Th3;
then
A8: p
in
[.r, t.[ by
A7,
Th3;
not p
in
[.r, s.[ by
A6,
Th3;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:186
Th186: r
<= s implies (
[.r, t.]
\
[.r, s.])
=
].s, t.]
proof
assume that
A1: r
<= s;
let p;
thus p
in (
[.r, t.]
\
[.r, s.]) implies p
in
].s, t.]
proof
assume
A2: p
in (
[.r, t.]
\
[.r, s.]);
then
A3: not p
in
[.r, s.] by
XBOOLE_0:def 5;
A4: p
<= t by
A2,
Th1;
p
< r or s
< p by
A3,
Th1;
hence thesis by
A2,
A4,
Th1,
Th2;
end;
assume
A5: p
in
].s, t.];
then
A6: s
< p by
Th2;
then
A7: r
<= p by
A1,
XXREAL_0: 2;
p
<= t by
A5,
Th2;
then
A8: p
in
[.r, t.] by
A7,
Th1;
not p
in
[.r, s.] by
A6,
Th1;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:187
Th187: r
< s implies (
].r, t.[
\
].r, s.])
=
].s, t.[
proof
assume that
A1: r
< s;
let p;
thus p
in (
].r, t.[
\
].r, s.]) implies p
in
].s, t.[
proof
assume
A2: p
in (
].r, t.[
\
].r, s.]);
then
A3: not p
in
].r, s.] by
XBOOLE_0:def 5;
A4: p
< t by
A2,
Th4;
p
<= r or s
< p by
A3,
Th2;
hence thesis by
A2,
A4,
Th4;
end;
assume
A5: p
in
].s, t.[;
then
A6: s
< p by
Th4;
then
A7: r
< p by
A1,
XXREAL_0: 2;
p
< t by
A5,
Th4;
then
A8: p
in
].r, t.[ by
A7,
Th4;
not p
in
].r, s.] by
A6,
Th2;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:188
Th188: r
< s implies (
].r, t.]
\
].r, s.[)
=
[.s, t.]
proof
assume that
A1: r
< s;
let p;
thus p
in (
].r, t.]
\
].r, s.[) implies p
in
[.s, t.]
proof
assume
A2: p
in (
].r, t.]
\
].r, s.[);
then
A3: not p
in
].r, s.[ by
XBOOLE_0:def 5;
A4: p
<= t by
A2,
Th2;
p
<= r or s
<= p by
A3,
Th4;
hence thesis by
A2,
A4,
Th1,
Th2;
end;
assume
A5: p
in
[.s, t.];
then
A6: s
<= p by
Th1;
then
A7: r
< p by
A1,
XXREAL_0: 2;
p
<= t by
A5,
Th1;
then
A8: p
in
].r, t.] by
A7,
Th2;
not p
in
].r, s.[ by
A6,
Th4;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:189
Th189: r
< s implies (
].r, t.[
\
].r, s.[)
=
[.s, t.[
proof
assume that
A1: r
< s;
let p;
thus p
in (
].r, t.[
\
].r, s.[) implies p
in
[.s, t.[
proof
assume
A2: p
in (
].r, t.[
\
].r, s.[);
then
A3: not p
in
].r, s.[ by
XBOOLE_0:def 5;
A4: p
< t by
A2,
Th4;
p
<= r or s
<= p by
A3,
Th4;
hence thesis by
A2,
A4,
Th3,
Th4;
end;
assume
A5: p
in
[.s, t.[;
then
A6: s
<= p by
Th3;
then
A7: r
< p by
A1,
XXREAL_0: 2;
p
< t by
A5,
Th3;
then
A8: p
in
].r, t.[ by
A7,
Th4;
not p
in
].r, s.[ by
A6,
Th4;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:190
Th190: s
<= t implies (
[.r, t.]
\
[.s, t.])
=
[.r, s.[
proof
assume that
A1: s
<= t;
let p;
thus p
in (
[.r, t.]
\
[.s, t.]) implies p
in
[.r, s.[
proof
assume
A2: p
in (
[.r, t.]
\
[.s, t.]);
then
A3: not p
in
[.s, t.] by
XBOOLE_0:def 5;
A4: r
<= p by
A2,
Th1;
p
< s or t
< p by
A3,
Th1;
hence thesis by
A2,
A4,
Th1,
Th3;
end;
assume
A5: p
in
[.r, s.[;
then
A6: p
< s by
Th3;
A7: r
<= p by
A5,
Th3;
p
<= t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
[.r, t.] by
A7,
Th1;
not p
in
[.s, t.] by
A6,
Th1;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:191
Th191: s
<= t implies (
].r, t.]
\
[.s, t.])
=
].r, s.[
proof
assume that
A1: s
<= t;
let p;
thus p
in (
].r, t.]
\
[.s, t.]) implies p
in
].r, s.[
proof
assume
A2: p
in (
].r, t.]
\
[.s, t.]);
then
A3: not p
in
[.s, t.] by
XBOOLE_0:def 5;
A4: r
< p by
A2,
Th2;
p
< s or t
< p by
A3,
Th1;
hence thesis by
A2,
A4,
Th2,
Th4;
end;
assume
A5: p
in
].r, s.[;
then
A6: p
< s by
Th4;
A7: r
< p by
A5,
Th4;
p
<= t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
].r, t.] by
A7,
Th2;
not p
in
[.s, t.] by
A6,
Th1;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:192
Th192: s
< t implies (
[.r, t.]
\
].s, t.])
=
[.r, s.]
proof
assume that
A1: s
< t;
let p;
thus p
in (
[.r, t.]
\
].s, t.]) implies p
in
[.r, s.]
proof
assume
A2: p
in (
[.r, t.]
\
].s, t.]);
then
A3: not p
in
].s, t.] by
XBOOLE_0:def 5;
A4: r
<= p by
A2,
Th1;
p
<= s or t
< p by
A3,
Th2;
hence thesis by
A2,
A4,
Th1;
end;
assume
A5: p
in
[.r, s.];
then
A6: p
<= s by
Th1;
A7: r
<= p by
A5,
Th1;
p
<= t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
[.r, t.] by
A7,
Th1;
not p
in
].s, t.] by
A6,
Th2;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:193
Th193: s
< t implies (
].r, t.]
\
].s, t.])
=
].r, s.]
proof
assume that
A1: s
< t;
let p;
thus p
in (
].r, t.]
\
].s, t.]) implies p
in
].r, s.]
proof
assume
A2: p
in (
].r, t.]
\
].s, t.]);
then
A3: not p
in
].s, t.] by
XBOOLE_0:def 5;
A4: r
< p by
A2,
Th2;
p
<= s or t
< p by
A3,
Th2;
hence thesis by
A2,
A4,
Th2;
end;
assume
A5: p
in
].r, s.];
then
A6: p
<= s by
Th2;
A7: r
< p by
A5,
Th2;
p
<= t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
].r, t.] by
A7,
Th2;
not p
in
].s, t.] by
A6,
Th2;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:194
Th194: s
< t implies (
[.r, t.[
\
[.s, t.[)
=
[.r, s.[
proof
assume that
A1: s
< t;
let p;
thus p
in (
[.r, t.[
\
[.s, t.[) implies p
in
[.r, s.[
proof
assume
A2: p
in (
[.r, t.[
\
[.s, t.[);
then
A3: not p
in
[.s, t.[ by
XBOOLE_0:def 5;
A4: r
<= p by
A2,
Th3;
p
< s or t
<= p by
A3,
Th3;
hence thesis by
A2,
A4,
Th3;
end;
assume
A5: p
in
[.r, s.[;
then
A6: p
< s by
Th3;
A7: r
<= p by
A5,
Th3;
p
< t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
[.r, t.[ by
A7,
Th3;
not p
in
[.s, t.[ by
A6,
Th3;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:195
Th195: s
< t implies (
].r, t.[
\
[.s, t.[)
=
].r, s.[
proof
assume that
A1: s
< t;
let p;
thus p
in (
].r, t.[
\
[.s, t.[) implies p
in
].r, s.[
proof
assume
A2: p
in (
].r, t.[
\
[.s, t.[);
then
A3: not p
in
[.s, t.[ by
XBOOLE_0:def 5;
A4: r
< p by
A2,
Th4;
p
< s or t
<= p by
A3,
Th3;
hence thesis by
A2,
A4,
Th4;
end;
assume
A5: p
in
].r, s.[;
then
A6: p
< s by
Th4;
A7: r
< p by
A5,
Th4;
p
< t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
].r, t.[ by
A7,
Th4;
not p
in
[.s, t.[ by
A6,
Th3;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:196
Th196: s
< t implies (
[.r, t.[
\
].s, t.[)
=
[.r, s.]
proof
assume that
A1: s
< t;
let p;
thus p
in (
[.r, t.[
\
].s, t.[) implies p
in
[.r, s.]
proof
assume
A2: p
in (
[.r, t.[
\
].s, t.[);
then
A3: not p
in
].s, t.[ by
XBOOLE_0:def 5;
A4: r
<= p by
A2,
Th3;
p
<= s or t
<= p by
A3,
Th4;
hence thesis by
A2,
A4,
Th1,
Th3;
end;
assume
A5: p
in
[.r, s.];
then
A6: p
<= s by
Th1;
A7: r
<= p by
A5,
Th1;
p
< t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
[.r, t.[ by
A7,
Th3;
not p
in
].s, t.[ by
A6,
Th4;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:197
Th197: s
< t implies (
].r, t.[
\
].s, t.[)
=
].r, s.]
proof
assume that
A1: s
< t;
let p;
thus p
in (
].r, t.[
\
].s, t.[) implies p
in
].r, s.]
proof
assume
A2: p
in (
].r, t.[
\
].s, t.[);
then
A3: not p
in
].s, t.[ by
XBOOLE_0:def 5;
A4: r
< p by
A2,
Th4;
p
<= s or t
<= p by
A3,
Th4;
hence thesis by
A2,
A4,
Th2,
Th4;
end;
assume
A5: p
in
].r, s.];
then
A6: p
<= s by
Th2;
A7: r
< p by
A5,
Th2;
p
< t by
A1,
A6,
XXREAL_0: 2;
then
A8: p
in
].r, t.[ by
A7,
Th4;
not p
in
].s, t.[ by
A6,
Th4;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:198
[.p, q.[
meets
[.r, s.[ implies (
[.p, q.[
\
[.r, s.[)
= (
[.p, r.[
\/
[.s, q.[)
proof
assume
[.p, q.[
meets
[.r, s.[;
then
consider u such that
A1: u
in
[.r, s.[ and
A2: u
in
[.p, q.[;
A3: r
<= u by
A1,
Th3;
A4: u
<= s by
A1,
Th3;
A5: p
<= u by
A2,
Th3;
u
<= q by
A2,
Th3;
then
A6: r
<= q by
A3,
XXREAL_0: 2;
A7: p
<= s by
A4,
A5,
XXREAL_0: 2;
let t;
thus t
in (
[.p, q.[
\
[.r, s.[) implies t
in (
[.p, r.[
\/
[.s, q.[)
proof
assume
A8: t
in (
[.p, q.[
\
[.r, s.[);
then
A9: not t
in
[.r, s.[ by
XBOOLE_0:def 5;
A10: p
<= t by
A8,
Th3;
A11: t
< q by
A8,
Th3;
t
< r or s
<= t by
A9,
Th3;
then t
in
[.p, r.[ or t
in
[.s, q.[ by
A10,
A11,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
assume t
in (
[.p, r.[
\/
[.s, q.[);
then t
in
[.p, r.[ or t
in
[.s, q.[ by
XBOOLE_0:def 3;
then
A12: p
<= t & t
< r or s
<= t & t
< q by
Th3;
then
A13: p
<= t by
A7,
XXREAL_0: 2;
t
< q by
A6,
A12,
XXREAL_0: 2;
then
A14: t
in
[.p, q.[ by
A13,
Th3;
not t
in
[.r, s.[ by
A12,
Th3;
hence thesis by
A14,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:199
].p, q.]
meets
].r, s.] implies (
].p, q.]
\
].r, s.])
= (
].p, r.]
\/
].s, q.])
proof
assume
].p, q.]
meets
].r, s.];
then
consider u such that
A1: u
in
].r, s.] and
A2: u
in
].p, q.];
A3: r
< u by
A1,
Th2;
A4: u
<= s by
A1,
Th2;
A5: p
< u by
A2,
Th2;
u
<= q by
A2,
Th2;
then
A6: r
<= q by
A3,
XXREAL_0: 2;
A7: p
<= s by
A4,
A5,
XXREAL_0: 2;
let t;
thus t
in (
].p, q.]
\
].r, s.]) implies t
in (
].p, r.]
\/
].s, q.])
proof
assume
A8: t
in (
].p, q.]
\
].r, s.]);
then
A9: not t
in
].r, s.] by
XBOOLE_0:def 5;
A10: p
< t by
A8,
Th2;
A11: t
<= q by
A8,
Th2;
t
<= r or s
< t by
A9,
Th2;
then t
in
].p, r.] or t
in
].s, q.] by
A10,
A11,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
assume t
in (
].p, r.]
\/
].s, q.]);
then t
in
].p, r.] or t
in
].s, q.] by
XBOOLE_0:def 3;
then
A12: p
< t & t
<= r or s
< t & t
<= q by
Th2;
then
A13: p
< t by
A7,
XXREAL_0: 2;
t
<= q by
A6,
A12,
XXREAL_0: 2;
then
A14: t
in
].p, q.] by
A13,
Th2;
not t
in
].r, s.] by
A12,
Th2;
hence thesis by
A14,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:200
p
<= r & s
<= q implies (
[.p, q.]
\ (
[.p, r.]
\/
[.s, q.]))
=
].r, s.[
proof
assume that
A1: p
<= r and
A2: s
<= q;
thus (
[.p, q.]
\ (
[.p, r.]
\/
[.s, q.]))
= ((
[.p, q.]
\
[.p, r.])
\
[.s, q.]) by
XBOOLE_1: 41
.= (
].r, q.]
\
[.s, q.]) by
A1,
Th182
.=
].r, s.[ by
A2,
Th191;
end;
theorem ::
XXREAL_1:201
r
<= s & s
<= t implies (
[.r, t.]
\
{s})
= (
[.r, s.[
\/
].s, t.])
proof
assume that
A1: r
<= s and
A2: s
<= t;
let p;
thus p
in (
[.r, t.]
\
{s}) implies p
in (
[.r, s.[
\/
].s, t.])
proof
assume
A3: p
in (
[.r, t.]
\
{s});
then not p
in
{s} by
XBOOLE_0:def 5;
then p
<> s by
TARSKI:def 1;
then r
<= p & p
< s or s
< p & p
<= t by
A3,
Th1,
XXREAL_0: 1;
then p
in
[.r, s.[ or p
in
].s, t.] by
Th2,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
assume p
in (
[.r, s.[
\/
].s, t.]);
then p
in
[.r, s.[ or p
in
].s, t.] by
XBOOLE_0:def 3;
then
A4: r
<= p & p
< s or s
< p & p
<= t by
Th2,
Th3;
then
A5: r
<= p by
A1,
XXREAL_0: 2;
p
<= t by
A2,
A4,
XXREAL_0: 2;
then
A6: p
in
[.r, t.] by
A5,
Th1;
not p
in
{s} by
A4,
TARSKI:def 1;
hence thesis by
A6,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:202
r
<= s & s
< t implies (
[.r, t.[
\
{s})
= (
[.r, s.[
\/
].s, t.[)
proof
assume that
A1: r
<= s and
A2: s
< t;
let p;
thus p
in (
[.r, t.[
\
{s}) implies p
in (
[.r, s.[
\/
].s, t.[)
proof
assume
A3: p
in (
[.r, t.[
\
{s});
then not p
in
{s} by
XBOOLE_0:def 5;
then p
<> s by
TARSKI:def 1;
then r
<= p & p
< s or s
< p & p
< t by
A3,
Th3,
XXREAL_0: 1;
then p
in
[.r, s.[ or p
in
].s, t.[ by
Th3,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume p
in (
[.r, s.[
\/
].s, t.[);
then p
in
[.r, s.[ or p
in
].s, t.[ by
XBOOLE_0:def 3;
then
A4: r
<= p & p
< s or s
< p & p
< t by
Th3,
Th4;
then
A5: r
<= p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A4,
XXREAL_0: 2;
then
A6: p
in
[.r, t.[ by
A5,
Th3;
not p
in
{s} by
A4,
TARSKI:def 1;
hence thesis by
A6,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:203
r
< s & s
<= t implies (
].r, t.]
\
{s})
= (
].r, s.[
\/
].s, t.])
proof
assume that
A1: r
< s and
A2: s
<= t;
let p;
thus p
in (
].r, t.]
\
{s}) implies p
in (
].r, s.[
\/
].s, t.])
proof
assume
A3: p
in (
].r, t.]
\
{s});
then not p
in
{s} by
XBOOLE_0:def 5;
then p
<> s by
TARSKI:def 1;
then r
< p & p
< s or s
< p & p
<= t by
A3,
Th2,
XXREAL_0: 1;
then p
in
].r, s.[ or p
in
].s, t.] by
Th2,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume p
in (
].r, s.[
\/
].s, t.]);
then p
in
].r, s.[ or p
in
].s, t.] by
XBOOLE_0:def 3;
then
A4: r
< p & p
< s or s
< p & p
<= t by
Th2,
Th4;
then
A5: r
< p by
A1,
XXREAL_0: 2;
p
<= t by
A2,
A4,
XXREAL_0: 2;
then
A6: p
in
].r, t.] by
A5,
Th2;
not p
in
{s} by
A4,
TARSKI:def 1;
hence thesis by
A6,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:204
r
< s & s
< t implies (
].r, t.[
\
{s})
= (
].r, s.[
\/
].s, t.[)
proof
assume that
A1: r
< s and
A2: s
< t;
let p;
thus p
in (
].r, t.[
\
{s}) implies p
in (
].r, s.[
\/
].s, t.[)
proof
assume
A3: p
in (
].r, t.[
\
{s});
then not p
in
{s} by
XBOOLE_0:def 5;
then p
<> s by
TARSKI:def 1;
then r
< p & p
< s or s
< p & p
< t by
A3,
Th4,
XXREAL_0: 1;
then p
in
].r, s.[ or p
in
].s, t.[ by
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume p
in (
].r, s.[
\/
].s, t.[);
then p
in
].r, s.[ or p
in
].s, t.[ by
XBOOLE_0:def 3;
then
A4: r
< p & p
< s or s
< p & p
< t by
Th4;
then
A5: r
< p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A4,
XXREAL_0: 2;
then
A6: p
in
].r, t.[ by
A5,
Th4;
not p
in
{s} by
A4,
TARSKI:def 1;
hence thesis by
A6,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:205
not s
in (
].r, s.[
\/
].s, t.[)
proof
assume s
in (
].r, s.[
\/
].s, t.[);
then s
in
].r, s.[ or s
in
].s, t.[ by
XBOOLE_0:def 3;
hence contradiction by
Th4;
end;
theorem ::
XXREAL_1:206
not s
in (
[.r, s.[
\/
].s, t.[)
proof
assume s
in (
[.r, s.[
\/
].s, t.[);
then s
in
[.r, s.[ or s
in
].s, t.[ by
XBOOLE_0:def 3;
hence contradiction by
Th3,
Th4;
end;
theorem ::
XXREAL_1:207
not s
in (
].r, s.[
\/
].s, t.])
proof
assume s
in (
].r, s.[
\/
].s, t.]);
then s
in
].r, s.[ or s
in
].s, t.] by
XBOOLE_0:def 3;
hence contradiction by
Th2,
Th4;
end;
theorem ::
XXREAL_1:208
not s
in (
[.r, s.[
\/
].s, t.])
proof
assume s
in (
[.r, s.[
\/
].s, t.]);
then s
in
[.r, s.[ or s
in
].s, t.] by
XBOOLE_0:def 3;
hence contradiction by
Th2,
Th3;
end;
begin
theorem ::
XXREAL_1:209
[.
-infty ,
+infty .]
=
ExtREAL
proof
let r;
thus r
in
[.
-infty ,
+infty .] implies r
in
ExtREAL by
XXREAL_0:def 1;
assume r
in
ExtREAL ;
A1:
-infty
<= r by
XXREAL_0: 5;
r
<=
+infty by
XXREAL_0: 3;
hence thesis by
A1,
Th1;
end;
theorem ::
XXREAL_1:210
].p,
-infty .[
=
{}
proof
not ex x be
object st x
in
].p,
-infty .[
proof
given x be
object such that
A1: x
in
].p,
-infty .[;
reconsider s = x as
ExtReal by
A1;
s
<
-infty by
A1,
Th4;
hence contradiction by
XXREAL_0: 5;
end;
hence thesis;
end;
theorem ::
XXREAL_1:211
[.p,
-infty .[
=
{}
proof
not ex x be
object st x
in
[.p,
-infty .[
proof
given x be
object such that
A1: x
in
[.p,
-infty .[;
reconsider s = x as
ExtReal by
A1;
s
<
-infty by
A1,
Th3;
hence contradiction by
XXREAL_0: 5;
end;
hence thesis;
end;
theorem ::
XXREAL_1:212
].p,
-infty .]
=
{}
proof
not ex x be
object st x
in
].p,
-infty .]
proof
given x be
object such that
A1: x
in
].p,
-infty .];
reconsider s = x as
ExtReal by
A1;
A2: p
< s by
A1,
Th2;
s
<=
-infty by
A1,
Th2;
then p
<
-infty by
A2,
XXREAL_0: 2;
hence contradiction by
XXREAL_0: 5;
end;
hence thesis;
end;
theorem ::
XXREAL_1:213
p
<>
-infty implies
[.p,
-infty .]
=
{}
proof
assume
A1: p
<>
-infty ;
not ex x be
object st x
in
[.p,
-infty .]
proof
given x be
object such that
A2: x
in
[.p,
-infty .];
reconsider s = x as
ExtReal by
A2;
A3: p
<= s by
A2,
Th1;
s
<=
-infty by
A2,
Th1;
hence contradiction by
A1,
A3,
XXREAL_0: 2,
XXREAL_0: 6;
end;
hence thesis;
end;
theorem ::
XXREAL_1:214
].
+infty , p.[
=
{}
proof
not ex x be
object st x
in
].
+infty , p.[
proof
given x be
object such that
A1: x
in
].
+infty , p.[;
reconsider s = x as
ExtReal by
A1;
+infty
< s by
A1,
Th4;
hence contradiction by
XXREAL_0: 3;
end;
hence thesis;
end;
theorem ::
XXREAL_1:215
[.
+infty , p.[
=
{}
proof
not ex x be
object st x
in
[.
+infty , p.[
proof
given x be
object such that
A1: x
in
[.
+infty , p.[;
reconsider s = x as
ExtReal by
A1;
A2:
+infty
<= s by
A1,
Th3;
s
< p by
A1,
Th3;
then p
>
+infty by
A2,
XXREAL_0: 2;
hence contradiction by
XXREAL_0: 3;
end;
hence thesis;
end;
theorem ::
XXREAL_1:216
].
+infty , p.]
=
{}
proof
not ex x be
object st x
in
].
+infty , p.]
proof
given x be
object such that
A1: x
in
].
+infty , p.];
reconsider s = x as
ExtReal by
A1;
+infty
< s by
A1,
Th2;
hence contradiction by
XXREAL_0: 3;
end;
hence thesis;
end;
theorem ::
XXREAL_1:217
p
<>
+infty implies
[.
+infty , p.]
=
{}
proof
assume
A1: p
<>
+infty ;
not ex x be
object st x
in
[.
+infty , p.]
proof
given x be
object such that
A2: x
in
[.
+infty , p.];
reconsider s = x as
ExtReal by
A2;
A3:
+infty
<= s by
A2,
Th1;
s
<= p by
A2,
Th1;
hence contradiction by
A1,
A3,
XXREAL_0: 2,
XXREAL_0: 4;
end;
hence thesis;
end;
theorem ::
XXREAL_1:218
p
> q implies p
in
].q,
+infty .] by
XXREAL_0: 3,
Th2;
theorem ::
XXREAL_1:219
q
<= p implies p
in
[.q,
+infty .]
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th1;
end;
theorem ::
XXREAL_1:220
p
<= q implies p
in
[.
-infty , q.]
proof
p
>=
-infty by
XXREAL_0: 5;
hence thesis by
Th1;
end;
theorem ::
XXREAL_1:221
p
< q implies p
in
[.
-infty , q.[ by
XXREAL_0: 5,
Th3;
begin
theorem ::
XXREAL_1:222
p
<= q implies
[.p, q.]
= (
[.p, q.]
\/
[.q, p.])
proof
assume
A1: p
<= q;
then
A2:
[.q, p.]
c=
{p} by
Th85;
p
in
[.p, q.] by
A1,
Th1;
then
{p}
c=
[.p, q.] by
ZFMISC_1: 31;
hence thesis by
A2,
XBOOLE_1: 1,
XBOOLE_1: 12;
end;
theorem ::
XXREAL_1:223
r
<= s & s
<= t implies not r
in (
].s, t.[
\/
].t, p.[)
proof
assume that
A1: r
<= s and
A2: s
<= t;
assume r
in (
].s, t.[
\/
].t, p.[);
then r
in
].s, t.[ or r
in
].t, p.[ by
XBOOLE_0:def 3;
then s
< r & r
< t or t
< r & r
< p by
Th4;
hence contradiction by
A1,
A2,
XXREAL_0: 2;
end;
theorem ::
XXREAL_1:224
Th224:
REAL
=
].
-infty ,
+infty .[
proof
let x be
ExtReal;
thus x
in
REAL implies x
in
].
-infty ,
+infty .[
proof
assume
A1: x
in
REAL ;
then
A2:
-infty
< x by
XXREAL_0: 12;
x
<
+infty by
A1,
XXREAL_0: 9;
hence thesis by
A2,
Th4;
end;
assume
A3: x
in
].
-infty ,
+infty .[;
then
A4:
-infty
< x by
Th4;
x
<
+infty by
A3,
Th4;
hence thesis by
A4,
XXREAL_0: 14;
end;
theorem ::
XXREAL_1:225
Th225:
].p, q.[
c=
REAL
proof
let x be
ExtReal;
assume
A1: x
in
].p, q.[;
then
A2: p
< x by
Th4;
x
< q by
A1,
Th4;
hence thesis by
A2,
XXREAL_0: 48;
end;
theorem ::
XXREAL_1:226
Th226: p
in
REAL implies
[.p, q.[
c=
REAL
proof
assume
A1: p
in
REAL ;
let x be
ExtReal;
assume
A2: x
in
[.p, q.[;
then
A3: p
<= x by
Th3;
x
< q by
A2,
Th3;
hence thesis by
A1,
A3,
XXREAL_0: 46;
end;
theorem ::
XXREAL_1:227
Th227: q
in
REAL implies
].p, q.]
c=
REAL
proof
assume
A1: q
in
REAL ;
let x be
ExtReal;
assume
A2: x
in
].p, q.];
then
A3: p
< x by
Th2;
x
<= q by
A2,
Th2;
hence thesis by
A1,
A3,
XXREAL_0: 47;
end;
theorem ::
XXREAL_1:228
Th228: p
in
REAL & q
in
REAL implies
[.p, q.]
c=
REAL
proof
assume that
A1: p
in
REAL and
A2: q
in
REAL ;
let x be
ExtReal;
assume
A3: x
in
[.p, q.];
then
A4: p
<= x by
Th1;
x
<= q by
A3,
Th1;
hence thesis by
A1,
A2,
A4,
XXREAL_0: 45;
end;
registration
let p, q;
cluster
].p, q.[ ->
real-membered;
coherence by
Th225,
MEMBERED: 21;
end
registration
let p be
Real, q;
cluster
[.p, q.[ ->
real-membered;
coherence
proof
p
in
REAL by
XREAL_0:def 1;
then
[.p, q.[
c=
REAL by
Th226;
hence thesis;
end;
end
registration
let q be
Real, p;
cluster
].p, q.] ->
real-membered;
coherence
proof
q
in
REAL by
XREAL_0:def 1;
then
].p, q.]
c=
REAL by
Th227;
hence thesis;
end;
end
registration
let p,q be
Real;
cluster
[.p, q.] ->
real-membered;
coherence
proof
A1: p
in
REAL by
XREAL_0:def 1;
q
in
REAL by
XREAL_0:def 1;
then
[.p, q.]
c=
REAL by
A1,
Th228;
hence thesis;
end;
end
theorem ::
XXREAL_1:229
].
-infty , s.[
= { g : g
< s }
proof
thus
].
-infty , s.[
c= { g : g
< s }
proof
let x be
Real;
assume
A1: x
in
].
-infty , s.[;
A2: x
< s by
A1,
Th4;
thus thesis by
A2;
end;
let x be
object;
assume x
in { g : g
< s };
then
consider g such that
A3: x
= g and
A4: g
< s;
g
in
REAL by
XREAL_0:def 1;
then
-infty
< g by
XXREAL_0: 12;
hence thesis by
A3,
A4,
Th4;
end;
theorem ::
XXREAL_1:230
].s,
+infty .[
= { g : s
< g }
proof
thus
].s,
+infty .[
c= { g : s
< g }
proof
let x be
Real;
assume x
in
].s,
+infty .[;
then
A1: s
< x by
Th4;
thus thesis by
A1;
end;
let x be
object;
assume x
in { g : s
< g };
then
consider g such that
A2: x
= g and
A3: s
< g;
g
in
REAL by
XREAL_0:def 1;
then g
<
+infty by
XXREAL_0: 9;
hence thesis by
A2,
A3,
Th4;
end;
theorem ::
XXREAL_1:231
for s be
Real holds
].
-infty , s.]
= { g : g
<= s }
proof
let s be
Real;
thus
].
-infty , s.]
c= { g : g
<= s }
proof
let x be
Real;
assume x
in
].
-infty , s.];
then
A1: x
<= s by
Th2;
thus thesis by
A1;
end;
let x be
object;
assume x
in { g : g
<= s };
then
consider g such that
A2: x
= g and
A3: g
<= s;
g
in
REAL by
XREAL_0:def 1;
then
-infty
< g by
XXREAL_0: 12;
hence thesis by
A2,
A3,
Th2;
end;
theorem ::
XXREAL_1:232
for s be
Real holds
[.s,
+infty .[
= { g : s
<= g }
proof
let s be
Real;
thus
[.s,
+infty .[
c= { g : s
<= g }
proof
let x be
Real;
assume x
in
[.s,
+infty .[;
then
A1: s
<= x by
Th3;
thus thesis by
A1;
end;
let x be
object;
assume x
in { g : s
<= g };
then
consider g such that
A2: x
= g and
A3: s
<= g;
g
in
REAL by
XREAL_0:def 1;
then g
<
+infty by
XXREAL_0: 9;
hence thesis by
A2,
A3,
Th3;
end;
theorem ::
XXREAL_1:233
for x be
Real holds x
in
].
-infty , u.[ iff x
< u
proof
let x be
Real;
x
in
REAL by
XREAL_0:def 1;
then
-infty
< x by
XXREAL_0: 12;
hence thesis by
Th4;
end;
theorem ::
XXREAL_1:234
for x be
Real holds x
in
].
-infty , u.] iff x
<= u
proof
let x be
Real;
x
in
REAL by
XREAL_0:def 1;
then
-infty
< x by
XXREAL_0: 12;
hence thesis by
Th2;
end;
theorem ::
XXREAL_1:235
for x be
Real holds x
in
].u,
+infty .[ iff u
< x
proof
let x be
Real;
x
in
REAL by
XREAL_0:def 1;
then x
<
+infty by
XXREAL_0: 9;
hence thesis by
Th4;
end;
theorem ::
XXREAL_1:236
for x be
Real holds x
in
[.u,
+infty .[ iff u
<= x
proof
let x be
Real;
x
in
REAL by
XREAL_0:def 1;
then x
<
+infty by
XXREAL_0: 9;
hence thesis by
Th3;
end;
theorem ::
XXREAL_1:237
p
<= r implies
[.r, s.]
c=
[.p,
+infty .]
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th34;
end;
theorem ::
XXREAL_1:238
p
<= r implies
[.r, s.[
c=
[.p,
+infty .]
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th35;
end;
theorem ::
XXREAL_1:239
p
<= r implies
].r, s.]
c=
[.p,
+infty .]
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th36;
end;
theorem ::
XXREAL_1:240
p
<= r implies
].r, s.[
c=
[.p,
+infty .]
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th37;
end;
theorem ::
XXREAL_1:241
p
<= r implies
[.r, s.[
c=
[.p,
+infty .[
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th38;
end;
theorem ::
XXREAL_1:242
p
< r implies
[.r, s.]
c=
].p,
+infty .] by
Th39,
XXREAL_0: 3;
theorem ::
XXREAL_1:243
p
< r implies
[.r, s.[
c=
].p,
+infty .] by
Th40,
XXREAL_0: 3;
theorem ::
XXREAL_1:244
p
<= r implies
].r, s.[
c=
].p,
+infty .]
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th41;
end;
theorem ::
XXREAL_1:245
p
<= r implies
].r, s.]
c=
].p,
+infty .]
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th42;
end;
theorem ::
XXREAL_1:246
p
<= r implies
].r, s.[
c=
[.p,
+infty .[
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th45;
end;
theorem ::
XXREAL_1:247
p
<= r implies
].r, s.[
c=
].p,
+infty .[
proof
s
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th46;
end;
theorem ::
XXREAL_1:248
p
< r implies
[.r, s.[
c=
].p,
+infty .[ by
Th48,
XXREAL_0: 3;
theorem ::
XXREAL_1:249
for s be
Real st p
< r holds
[.r, s.]
c=
].p,
+infty .[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
then s
<
+infty by
XXREAL_0: 9;
hence thesis by
Th47;
end;
theorem ::
XXREAL_1:250
for s be
Real st p
<= r holds
].r, s.]
c=
].p,
+infty .[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th49,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:251
for s be
Real st p
<= r holds
[.r, s.]
c=
[.p,
+infty .[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th43,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:252
for s be
Real st p
<= r holds
].r, s.]
c=
[.p,
+infty .[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th44,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:253
s
<= q implies
[.r, s.]
c=
[.
-infty , q.]
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th34;
end;
theorem ::
XXREAL_1:254
s
<= q implies
[.r, s.[
c=
[.
-infty , q.]
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th35;
end;
theorem ::
XXREAL_1:255
s
<= q implies
].r, s.]
c=
[.
-infty , q.]
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th36;
end;
theorem ::
XXREAL_1:256
s
<= q implies
].r, s.[
c=
[.
-infty , q.]
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th37;
end;
theorem ::
XXREAL_1:257
s
<= q implies
[.r, s.[
c=
[.
-infty , q.[
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th38;
end;
theorem ::
XXREAL_1:258
s
<= q implies
].r, s.[
c=
].
-infty , q.]
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th41;
end;
theorem ::
XXREAL_1:259
s
<= q implies
].r, s.]
c=
].
-infty , q.]
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th42;
end;
theorem ::
XXREAL_1:260
s
< q implies
[.r, s.]
c=
[.
-infty , q.[ by
Th43,
XXREAL_0: 5;
theorem ::
XXREAL_1:261
s
< q implies
].r, s.]
c=
[.
-infty , q.[ by
Th44,
XXREAL_0: 5;
theorem ::
XXREAL_1:262
s
<= q implies
].r, s.[
c=
[.
-infty , q.[
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th45;
end;
theorem ::
XXREAL_1:263
s
<= q implies
].r, s.[
c=
].
-infty , q.[
proof
-infty
<= r by
XXREAL_0: 5;
hence thesis by
Th46;
end;
theorem ::
XXREAL_1:264
s
< q implies
].r, s.]
c=
].
-infty , q.[ by
Th49,
XXREAL_0: 5;
theorem ::
XXREAL_1:265
for r be
Real st s
<= q holds
[.r, s.]
c=
].
-infty , q.]
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
hence thesis by
Th39,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:266
for r be
Real st s
<= q holds
[.r, s.[
c=
].
-infty , q.]
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
hence thesis by
Th40,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:267
for r be
Real st s
< q holds
[.r, s.]
c=
].
-infty , q.[
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
then
-infty
< r by
XXREAL_0: 12;
hence thesis by
Th47;
end;
theorem ::
XXREAL_1:268
for r be
Real st s
<= q holds
[.r, s.[
c=
].
-infty , q.[
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
hence thesis by
Th48,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:269
for a,b be
ExtReal holds (
].
-infty , b.[
/\
].a,
+infty .[)
=
].a, b.[
proof
let a,b be
ExtReal;
A1:
-infty
<= a by
XXREAL_0: 5;
b
<=
+infty by
XXREAL_0: 3;
hence thesis by
A1,
Th160;
end;
theorem ::
XXREAL_1:270
for b be
Real holds (
].
-infty , b.]
/\
].p,
+infty .[)
=
].p, b.]
proof
let b be
Real;
A1: b
in
REAL by
XREAL_0:def 1;
-infty
<= p by
XXREAL_0: 5;
hence thesis by
A1,
Th159,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:271
for a be
Real holds (
].
-infty , p.[
/\
[.a,
+infty .[)
=
[.a, p.[
proof
let a be
Real;
a
in
REAL by
XREAL_0:def 1;
then
-infty
< a by
XXREAL_0: 12;
hence thesis by
Th154,
XXREAL_0: 3;
end;
theorem ::
XXREAL_1:272
for a,b be
Real holds (
].
-infty , a.]
/\
[.b,
+infty .[)
=
[.b, a.]
proof
let a,b be
Real;
A1: a
in
REAL by
XREAL_0:def 1;
b
in
REAL by
XREAL_0:def 1;
then
A2:
-infty
< b by
XXREAL_0: 12;
a
<
+infty by
A1,
XXREAL_0: 9;
hence thesis by
A2,
Th152;
end;
theorem ::
XXREAL_1:273
s
<= p implies
[.r, s.[
misses
].p, q.[
proof
assume
A1: s
<= p;
let t;
assume t
in
[.r, s.[;
then t
<= s by
Th3;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th4;
end;
theorem ::
XXREAL_1:274
s
<= p implies
[.r, s.[
misses
].p, q.]
proof
assume
A1: s
<= p;
let t;
assume t
in
[.r, s.[;
then t
<= s by
Th3;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th2;
end;
theorem ::
XXREAL_1:275
s
<= p implies
].r, s.[
misses
].p, q.[
proof
assume
A1: s
<= p;
let t be
Real;
assume t
in
].r, s.[;
then t
<= s by
Th4;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th4;
end;
theorem ::
XXREAL_1:276
s
<= p implies
].r, s.[
misses
].p, q.]
proof
assume
A1: s
<= p;
let t;
assume t
in
].r, s.[;
then t
<= s by
Th4;
then t
<= p by
A1,
XXREAL_0: 2;
hence thesis by
Th2;
end;
theorem ::
XXREAL_1:277
s
< p implies
[.r, s.]
misses
[.p, q.[
proof
assume
A1: s
< p;
let t;
assume t
in
[.r, s.];
then t
<= s by
Th1;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th3;
end;
theorem ::
XXREAL_1:278
s
< p implies
[.r, s.]
misses
[.p, q.]
proof
assume
A1: s
< p;
let t;
assume t
in
[.r, s.];
then t
<= s by
Th1;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th1;
end;
theorem ::
XXREAL_1:279
s
< p implies
].r, s.]
misses
[.p, q.[
proof
assume
A1: s
< p;
let t;
assume t
in
].r, s.];
then t
<= s by
Th2;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th3;
end;
theorem ::
XXREAL_1:280
s
< p implies
].r, s.]
misses
[.p, q.]
proof
assume
A1: s
< p;
let t;
assume t
in
].r, s.];
then t
<= s by
Th2;
then t
< p by
A1,
XXREAL_0: 2;
hence thesis by
Th1;
end;
theorem ::
XXREAL_1:281
(
[.
-infty , t.]
\
[.
-infty , s.])
=
].s, t.] by
Th182,
XXREAL_0: 5;
theorem ::
XXREAL_1:282
(
[.
-infty , t.[
\
[.
-infty , s.])
=
].s, t.[ by
Th183,
XXREAL_0: 5;
theorem ::
XXREAL_1:283
(
[.
-infty , t.]
\
[.
-infty , s.])
=
].s, t.] by
Th186,
XXREAL_0: 5;
theorem ::
XXREAL_1:284
(
[.r,
+infty .]
\
[.s,
+infty .])
=
[.r, s.[ by
Th190,
XXREAL_0: 3;
theorem ::
XXREAL_1:285
(
].r,
+infty .]
\
[.s,
+infty .])
=
].r, s.[ by
Th191,
XXREAL_0: 3;
theorem ::
XXREAL_1:286
for s be
Real holds (
[.
-infty , t.]
\
[.
-infty , s.[)
=
[.s, t.]
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th184,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:287
for s be
Real holds (
[.
-infty , t.[
\
[.
-infty , s.[)
=
[.s, t.[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th185,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:288
for s be
Real holds (
].
-infty , t.[
\
].
-infty , s.])
=
].s, t.[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th187,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:289
for s be
Real holds (
].
-infty , t.]
\
].
-infty , s.[)
=
[.s, t.]
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th188,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:290
for s be
Real holds (
].
-infty , t.[
\
].
-infty , s.[)
=
[.s, t.[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th189,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:291
for s be
Real holds (
[.r,
+infty .]
\
].s,
+infty .])
=
[.r, s.]
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th192,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:292
for s be
Real holds (
].r,
+infty .]
\
].s,
+infty .])
=
].r, s.]
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th193,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:293
for s be
Real holds (
[.r,
+infty .[
\
[.s,
+infty .[)
=
[.r, s.[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th194,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:294
for s be
Real holds (
].r,
+infty .[
\
[.s,
+infty .[)
=
].r, s.[
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th195,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:295
for s be
Real holds (
[.r,
+infty .[
\
].s,
+infty .[)
=
[.r, s.]
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th196,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:296
for s be
Real holds (
].r,
+infty .[
\
].s,
+infty .[)
=
].r, s.]
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th197,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:297
Th297: r
< s & p
< q implies (
].r, q.[
\
].p, s.[)
= (
].r, p.]
\/
[.s, q.[)
proof
assume that
A1: r
< s and
A2: p
< q;
let x be
ExtReal;
thus x
in (
].r, q.[
\
].p, s.[) implies x
in (
].r, p.]
\/
[.s, q.[)
proof
assume
A3: x
in (
].r, q.[
\
].p, s.[);
then
A4: not x
in
].p, s.[ by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th4;
A6: x
< q by
A3,
Th4;
not (p
< x & x
< s) by
A4,
Th4;
then x
in
].r, p.] or x
in
[.s, q.[ by
A5,
A6,
Th2,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.]
\/
[.s, q.[);
then x
in
].r, p.] or x
in
[.s, q.[ by
XBOOLE_0:def 3;
then
A7: r
< x & x
<= p or s
<= x & x
< q by
Th2,
Th3;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.[ by
A8,
Th4;
not x
in
].p, s.[ by
A7,
Th4;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:298
Th298: r
<= s & p
< q implies (
[.r, q.[
\
].p, s.[)
= (
[.r, p.]
\/
[.s, q.[)
proof
assume that
A1: r
<= s and
A2: p
< q;
let x be
ExtReal;
thus x
in (
[.r, q.[
\
].p, s.[) implies x
in (
[.r, p.]
\/
[.s, q.[)
proof
assume
A3: x
in (
[.r, q.[
\
].p, s.[);
then
A4: not x
in
].p, s.[ by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th3;
A6: x
< q by
A3,
Th3;
not (p
< x & x
< s) by
A4,
Th4;
then x
in
[.r, p.] or x
in
[.s, q.[ by
A5,
A6,
Th1,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.]
\/
[.s, q.[);
then x
in
[.r, p.] or x
in
[.s, q.[ by
XBOOLE_0:def 3;
then
A7: r
<= x & x
<= p or s
<= x & x
< q by
Th1,
Th3;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.[ by
A8,
Th3;
not x
in
].p, s.[ by
A7,
Th4;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:299
Th299: r
< s & p
<= q implies (
].r, q.]
\
].p, s.[)
= (
].r, p.]
\/
[.s, q.])
proof
assume that
A1: r
< s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
].r, q.]
\
].p, s.[) implies x
in (
].r, p.]
\/
[.s, q.])
proof
assume
A3: x
in (
].r, q.]
\
].p, s.[);
then
A4: not x
in
].p, s.[ by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th2;
A6: x
<= q by
A3,
Th2;
not (p
< x & x
< s) by
A4,
Th4;
then x
in
].r, p.] or x
in
[.s, q.] by
A5,
A6,
Th1,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.]
\/
[.s, q.]);
then x
in
].r, p.] or x
in
[.s, q.] by
XBOOLE_0:def 3;
then
A7: r
< x & x
<= p or s
<= x & x
<= q by
Th1,
Th2;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.] by
A8,
Th2;
not x
in
].p, s.[ by
A7,
Th4;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:300
Th300: r
<= s & p
<= q implies (
[.r, q.]
\
].p, s.[)
= (
[.r, p.]
\/
[.s, q.])
proof
assume that
A1: r
<= s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
[.r, q.]
\
].p, s.[) implies x
in (
[.r, p.]
\/
[.s, q.])
proof
assume
A3: x
in (
[.r, q.]
\
].p, s.[);
then
A4: not x
in
].p, s.[ by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th1;
A6: x
<= q by
A3,
Th1;
not (p
< x & x
< s) by
A4,
Th4;
then x
in
[.r, p.] or x
in
[.s, q.] by
A5,
A6,
Th1;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.]
\/
[.s, q.]);
then x
in
[.r, p.] or x
in
[.s, q.] by
XBOOLE_0:def 3;
then
A7: r
<= x & x
<= p or s
<= x & x
<= q by
Th1;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.] by
A8,
Th1;
not x
in
].p, s.[ by
A7,
Th4;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:301
Th301: r
< s & p
<= q implies (
].r, q.[
\
[.p, s.[)
= (
].r, p.[
\/
[.s, q.[)
proof
assume that
A1: r
< s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
].r, q.[
\
[.p, s.[) implies x
in (
].r, p.[
\/
[.s, q.[)
proof
assume
A3: x
in (
].r, q.[
\
[.p, s.[);
then
A4: not x
in
[.p, s.[ by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th4;
A6: x
< q by
A3,
Th4;
not (p
<= x & x
< s) by
A4,
Th3;
then x
in
].r, p.[ or x
in
[.s, q.[ by
A5,
A6,
Th3,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.[
\/
[.s, q.[);
then x
in
].r, p.[ or x
in
[.s, q.[ by
XBOOLE_0:def 3;
then
A7: r
< x & x
< p or s
<= x & x
< q by
Th3,
Th4;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.[ by
A8,
Th4;
not x
in
[.p, s.[ by
A7,
Th3;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:302
Th302: r
<= s & p
<= q implies (
[.r, q.[
\
[.p, s.[)
= (
[.r, p.[
\/
[.s, q.[)
proof
assume that
A1: r
<= s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
[.r, q.[
\
[.p, s.[) implies x
in (
[.r, p.[
\/
[.s, q.[)
proof
assume
A3: x
in (
[.r, q.[
\
[.p, s.[);
then
A4: not x
in
[.p, s.[ by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th3;
A6: x
< q by
A3,
Th3;
not (p
<= x & x
< s) by
A4,
Th3;
then x
in
[.r, p.[ or x
in
[.s, q.[ by
A5,
A6,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.[
\/
[.s, q.[);
then x
in
[.r, p.[ or x
in
[.s, q.[ by
XBOOLE_0:def 3;
then
A7: r
<= x & x
< p or s
<= x & x
< q by
Th3;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.[ by
A8,
Th3;
not x
in
[.p, s.[ by
A7,
Th3;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:303
Th303: r
< s & p
<= q implies (
].r, q.]
\
[.p, s.[)
= (
].r, p.[
\/
[.s, q.])
proof
assume that
A1: r
< s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
].r, q.]
\
[.p, s.[) implies x
in (
].r, p.[
\/
[.s, q.])
proof
assume
A3: x
in (
].r, q.]
\
[.p, s.[);
then
A4: not x
in
[.p, s.[ by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th2;
A6: x
<= q by
A3,
Th2;
not (p
<= x & x
< s) by
A4,
Th3;
then x
in
].r, p.[ or x
in
[.s, q.] by
A5,
A6,
Th1,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.[
\/
[.s, q.]);
then x
in
].r, p.[ or x
in
[.s, q.] by
XBOOLE_0:def 3;
then
A7: r
< x & x
< p or s
<= x & x
<= q by
Th1,
Th4;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.] by
A8,
Th2;
not x
in
[.p, s.[ by
A7,
Th3;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:304
Th304: r
<= s & p
<= q implies (
[.r, q.]
\
[.p, s.[)
= (
[.r, p.[
\/
[.s, q.])
proof
assume that
A1: r
<= s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
[.r, q.]
\
[.p, s.[) implies x
in (
[.r, p.[
\/
[.s, q.])
proof
assume
A3: x
in (
[.r, q.]
\
[.p, s.[);
then
A4: not x
in
[.p, s.[ by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th1;
A6: x
<= q by
A3,
Th1;
not (p
<= x & x
< s) by
A4,
Th3;
then x
in
[.r, p.[ or x
in
[.s, q.] by
A5,
A6,
Th1,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.[
\/
[.s, q.]);
then x
in
[.r, p.[ or x
in
[.s, q.] by
XBOOLE_0:def 3;
then
A7: r
<= x & x
< p or s
<= x & x
<= q by
Th1,
Th3;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.] by
A8,
Th1;
not x
in
[.p, s.[ by
A7,
Th3;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:305
Th305: r
< s & p
< q implies (
].r, q.[
\
].p, s.])
= (
].r, p.]
\/
].s, q.[)
proof
assume that
A1: r
< s and
A2: p
< q;
let x be
ExtReal;
thus x
in (
].r, q.[
\
].p, s.]) implies x
in (
].r, p.]
\/
].s, q.[)
proof
assume
A3: x
in (
].r, q.[
\
].p, s.]);
then
A4: not x
in
].p, s.] by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th4;
A6: x
< q by
A3,
Th4;
not (p
< x & x
<= s) by
A4,
Th2;
then x
in
].r, p.] or x
in
].s, q.[ by
A5,
A6,
Th2,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.]
\/
].s, q.[);
then x
in
].r, p.] or x
in
].s, q.[ by
XBOOLE_0:def 3;
then
A7: r
< x & x
<= p or s
< x & x
< q by
Th2,
Th4;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.[ by
A8,
Th4;
not x
in
].p, s.] by
A7,
Th2;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:306
Th306: r
<= s & p
< q implies (
[.r, q.[
\
].p, s.])
= (
[.r, p.]
\/
].s, q.[)
proof
assume that
A1: r
<= s and
A2: p
< q;
let x be
ExtReal;
thus x
in (
[.r, q.[
\
].p, s.]) implies x
in (
[.r, p.]
\/
].s, q.[)
proof
assume
A3: x
in (
[.r, q.[
\
].p, s.]);
then
A4: not x
in
].p, s.] by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th3;
A6: x
< q by
A3,
Th3;
not (p
< x & x
<= s) by
A4,
Th2;
then x
in
[.r, p.] or x
in
].s, q.[ by
A5,
A6,
Th1,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.]
\/
].s, q.[);
then x
in
[.r, p.] or x
in
].s, q.[ by
XBOOLE_0:def 3;
then
A7: r
<= x & x
<= p or s
< x & x
< q by
Th1,
Th4;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.[ by
A8,
Th3;
not x
in
].p, s.] by
A7,
Th2;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:307
Th307: r
< s & p
<= q implies (
].r, q.]
\
].p, s.])
= (
].r, p.]
\/
].s, q.])
proof
assume that
A1: r
< s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
].r, q.]
\
].p, s.]) implies x
in (
].r, p.]
\/
].s, q.])
proof
assume
A3: x
in (
].r, q.]
\
].p, s.]);
then
A4: not x
in
].p, s.] by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th2;
A6: x
<= q by
A3,
Th2;
not (p
< x & x
<= s) by
A4,
Th2;
then x
in
].r, p.] or x
in
].s, q.] by
A5,
A6,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.]
\/
].s, q.]);
then x
in
].r, p.] or x
in
].s, q.] by
XBOOLE_0:def 3;
then
A7: r
< x & x
<= p or s
< x & x
<= q by
Th2;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.] by
A8,
Th2;
not x
in
].p, s.] by
A7,
Th2;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:308
Th308: r
<= s & p
<= q implies (
[.r, q.]
\
].p, s.])
= (
[.r, p.]
\/
].s, q.])
proof
assume that
A1: r
<= s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
[.r, q.]
\
].p, s.]) implies x
in (
[.r, p.]
\/
].s, q.])
proof
assume
A3: x
in (
[.r, q.]
\
].p, s.]);
then
A4: not x
in
].p, s.] by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th1;
A6: x
<= q by
A3,
Th1;
not (p
< x & x
<= s) by
A4,
Th2;
then x
in
[.r, p.] or x
in
].s, q.] by
A5,
A6,
Th1,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.]
\/
].s, q.]);
then x
in
[.r, p.] or x
in
].s, q.] by
XBOOLE_0:def 3;
then
A7: r
<= x & x
<= p or s
< x & x
<= q by
Th1,
Th2;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.] by
A8,
Th1;
not x
in
].p, s.] by
A7,
Th2;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:309
Th309: r
<= s & p
<= q implies (
].r, q.[
\
[.p, s.])
= (
].r, p.[
\/
].s, q.[)
proof
assume that
A1: r
<= s and
A2: p
<= q;
let x be
Real;
thus x
in (
].r, q.[
\
[.p, s.]) implies x
in (
].r, p.[
\/
].s, q.[)
proof
assume
A3: x
in (
].r, q.[
\
[.p, s.]);
then
A4: not x
in
[.p, s.] by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th4;
A6: x
< q by
A3,
Th4;
not (p
<= x & x
<= s) by
A4,
Th1;
then x
in
].r, p.[ or x
in
].s, q.[ by
A5,
A6,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.[
\/
].s, q.[);
then x
in
].r, p.[ or x
in
].s, q.[ by
XBOOLE_0:def 3;
then
A7: r
< x & x
< p or s
< x & x
< q by
Th4;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.[ by
A8,
Th4;
not x
in
[.p, s.] by
A7,
Th1;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:310
Th310: r
<= s & p
<= q implies (
[.r, q.[
\
[.p, s.])
= (
[.r, p.[
\/
].s, q.[)
proof
assume that
A1: r
<= s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
[.r, q.[
\
[.p, s.]) implies x
in (
[.r, p.[
\/
].s, q.[)
proof
assume
A3: x
in (
[.r, q.[
\
[.p, s.]);
then
A4: not x
in
[.p, s.] by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th3;
A6: x
< q by
A3,
Th3;
not (p
<= x & x
<= s) by
A4,
Th1;
then x
in
[.r, p.[ or x
in
].s, q.[ by
A5,
A6,
Th3,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.[
\/
].s, q.[);
then x
in
[.r, p.[ or x
in
].s, q.[ by
XBOOLE_0:def 3;
then
A7: r
<= x & x
< p or s
< x & x
< q by
Th3,
Th4;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
< q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.[ by
A8,
Th3;
not x
in
[.p, s.] by
A7,
Th1;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:311
Th311: r
< s & p
<= q implies (
].r, q.]
\
[.p, s.])
= (
].r, p.[
\/
].s, q.])
proof
assume that
A1: r
< s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
].r, q.]
\
[.p, s.]) implies x
in (
].r, p.[
\/
].s, q.])
proof
assume
A3: x
in (
].r, q.]
\
[.p, s.]);
then
A4: not x
in
[.p, s.] by
XBOOLE_0:def 5;
A5: r
< x by
A3,
Th2;
A6: x
<= q by
A3,
Th2;
not (p
<= x & x
<= s) by
A4,
Th1;
then x
in
].r, p.[ or x
in
].s, q.] by
A5,
A6,
Th2,
Th4;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
].r, p.[
\/
].s, q.]);
then x
in
].r, p.[ or x
in
].s, q.] by
XBOOLE_0:def 3;
then
A7: r
< x & x
< p or s
< x & x
<= q by
Th2,
Th4;
then
A8: r
< x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
].r, q.] by
A8,
Th2;
not x
in
[.p, s.] by
A7,
Th1;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:312
Th312: r
<= s & p
<= q implies (
[.r, q.]
\
[.p, s.])
= (
[.r, p.[
\/
].s, q.])
proof
assume that
A1: r
<= s and
A2: p
<= q;
let x be
ExtReal;
thus x
in (
[.r, q.]
\
[.p, s.]) implies x
in (
[.r, p.[
\/
].s, q.])
proof
assume
A3: x
in (
[.r, q.]
\
[.p, s.]);
then
A4: not x
in
[.p, s.] by
XBOOLE_0:def 5;
A5: r
<= x by
A3,
Th1;
A6: x
<= q by
A3,
Th1;
not (p
<= x & x
<= s) by
A4,
Th1;
then x
in
[.r, p.[ or x
in
].s, q.] by
A5,
A6,
Th2,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
assume x
in (
[.r, p.[
\/
].s, q.]);
then x
in
[.r, p.[ or x
in
].s, q.] by
XBOOLE_0:def 3;
then
A7: r
<= x & x
< p or s
< x & x
<= q by
Th2,
Th3;
then
A8: r
<= x by
A1,
XXREAL_0: 2;
x
<= q by
A2,
A7,
XXREAL_0: 2;
then
A9: x
in
[.r, q.] by
A8,
Th1;
not x
in
[.p, s.] by
A7,
Th1;
hence thesis by
A9,
XBOOLE_0:def 5;
end;
theorem ::
XXREAL_1:313
Th313: r
<= p & p
<= q implies (
].r, q.[
\
{p})
= (
].r, p.[
\/
].p, q.[)
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th309;
end;
theorem ::
XXREAL_1:314
Th314: r
<= p & p
<= q implies (
[.r, q.[
\
{p})
= (
[.r, p.[
\/
].p, q.[)
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th310;
end;
theorem ::
XXREAL_1:315
Th315: r
< p & p
<= q implies (
].r, q.]
\
{p})
= (
].r, p.[
\/
].p, q.])
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th311;
end;
theorem ::
XXREAL_1:316
Th316: r
<= p & p
<= q implies (
[.r, q.]
\
{p})
= (
[.r, p.[
\/
].p, q.])
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th312;
end;
theorem ::
XXREAL_1:317
Th317: r
< q & p
<= q implies (
].r, q.]
\
].p, q.[)
= (
].r, p.]
\/
{q})
proof
[.q, q.]
=
{q} by
Th17;
hence thesis by
Th299;
end;
theorem ::
XXREAL_1:318
Th318: r
<= q & p
<= q implies (
[.r, q.]
\
].p, q.[)
= (
[.r, p.]
\/
{q})
proof
[.q, q.]
=
{q} by
Th17;
hence thesis by
Th300;
end;
theorem ::
XXREAL_1:319
Th319: r
< q & p
<= q implies (
].r, q.]
\
[.p, q.[)
= (
].r, p.[
\/
{q})
proof
[.q, q.]
=
{q} by
Th17;
hence thesis by
Th303;
end;
theorem ::
XXREAL_1:320
Th320: r
<= q & p
<= q implies (
[.r, q.]
\
[.p, q.[)
= (
[.r, p.[
\/
{q})
proof
[.q, q.]
=
{q} by
Th17;
hence thesis by
Th304;
end;
theorem ::
XXREAL_1:321
Th321: p
<= s & p
< q implies (
[.p, q.[
\
].p, s.[)
= (
{p}
\/
[.s, q.[)
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th298;
end;
theorem ::
XXREAL_1:322
Th322: p
<= s & p
<= q implies (
[.p, q.]
\
].p, s.[)
= (
{p}
\/
[.s, q.])
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th300;
end;
theorem ::
XXREAL_1:323
Th323: p
<= s & p
< q implies (
[.p, q.[
\
].p, s.])
= (
{p}
\/
].s, q.[)
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th306;
end;
theorem ::
XXREAL_1:324
Th324: p
<= s & p
<= q implies (
[.p, q.]
\
].p, s.])
= (
{p}
\/
].s, q.])
proof
[.p, p.]
=
{p} by
Th17;
hence thesis by
Th308;
end;
theorem ::
XXREAL_1:325
Th325: p
< q implies (
[.
-infty , q.[
\
].p, s.[)
= (
[.
-infty , p.]
\/
[.s, q.[) by
Th298,
XXREAL_0: 5;
theorem ::
XXREAL_1:326
Th326: p
<= q implies (
[.
-infty , q.]
\
].p, s.[)
= (
[.
-infty , p.]
\/
[.s, q.])
proof
-infty
<= s by
XXREAL_0: 5;
hence thesis by
Th300;
end;
theorem ::
XXREAL_1:327
Th327: p
<= q implies (
[.
-infty , q.[
\
[.p, s.[)
= (
[.
-infty , p.[
\/
[.s, q.[)
proof
-infty
<= s by
XXREAL_0: 5;
hence thesis by
Th302;
end;
theorem ::
XXREAL_1:328
Th328: p
<= q implies (
[.
-infty , q.]
\
[.p, s.[)
= (
[.
-infty , p.[
\/
[.s, q.])
proof
-infty
<= s by
XXREAL_0: 5;
hence thesis by
Th304;
end;
theorem ::
XXREAL_1:329
Th329: p
< q implies (
[.
-infty , q.[
\
].p, s.])
= (
[.
-infty , p.]
\/
].s, q.[) by
Th306,
XXREAL_0: 5;
theorem ::
XXREAL_1:330
Th330: p
<= q implies (
[.
-infty , q.]
\
].p, s.])
= (
[.
-infty , p.]
\/
].s, q.])
proof
-infty
<= s by
XXREAL_0: 5;
hence thesis by
Th308;
end;
theorem ::
XXREAL_1:331
Th331: p
<= q implies (
[.
-infty , q.[
\
[.p, s.])
= (
[.
-infty , p.[
\/
].s, q.[)
proof
-infty
<= s by
XXREAL_0: 5;
hence thesis by
Th310;
end;
theorem ::
XXREAL_1:332
Th332: p
<= q implies (
[.
-infty , q.]
\
[.p, s.])
= (
[.
-infty , p.[
\/
].s, q.])
proof
-infty
<= s by
XXREAL_0: 5;
hence thesis by
Th312;
end;
theorem ::
XXREAL_1:333
Th333: for s be
Real holds p
< q implies (
].
-infty , q.[
\
].p, s.[)
= (
].
-infty , p.]
\/
[.s, q.[)
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
then
-infty
< s by
XXREAL_0: 12;
hence thesis by
Th297;
end;
theorem ::
XXREAL_1:334
Th334: for s be
Real holds p
<= q implies (
].
-infty , q.]
\
].p, s.[)
= (
].
-infty , p.]
\/
[.s, q.])
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th299,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:335
Th335: for s be
Real holds p
<= q implies (
].
-infty , q.[
\
[.p, s.[)
= (
].
-infty , p.[
\/
[.s, q.[)
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th301,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:336
Th336: for s be
Real holds p
<= q implies (
].
-infty , q.]
\
[.p, s.[)
= (
].
-infty , p.[
\/
[.s, q.])
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th303,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:337
Th337: for s be
Real holds p
< q implies (
].
-infty , q.[
\
].p, s.])
= (
].
-infty , p.]
\/
].s, q.[)
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
then
-infty
< s by
XXREAL_0: 12;
hence thesis by
Th305;
end;
theorem ::
XXREAL_1:338
Th338: for s be
Real holds p
<= q implies (
].
-infty , q.]
\
].p, s.])
= (
].
-infty , p.]
\/
].s, q.])
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th307,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:339
Th339: p
<= q implies (
].
-infty , q.[
\
[.p, s.])
= (
].
-infty , p.[
\/
].s, q.[)
proof
-infty
<= s by
XXREAL_0: 5;
hence thesis by
Th309;
end;
theorem ::
XXREAL_1:340
Th340: for s be
Real holds p
<= q implies (
].
-infty , q.]
\
[.p, s.])
= (
].
-infty , p.[
\/
].s, q.])
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th311,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:341
Th341: p
<= q implies (
[.
-infty , q.[
\
{p})
= (
[.
-infty , p.[
\/
].p, q.[)
proof
-infty
<= p by
XXREAL_0: 5;
hence thesis by
Th314;
end;
theorem ::
XXREAL_1:342
Th342: p
<= q implies (
[.
-infty , q.]
\
{p})
= (
[.
-infty , p.[
\/
].p, q.])
proof
-infty
<= p by
XXREAL_0: 5;
hence thesis by
Th316;
end;
theorem ::
XXREAL_1:343
p
<= q implies (
[.
-infty , q.]
\
].p, q.[)
= (
[.
-infty , p.]
\/
{q})
proof
-infty
<= q by
XXREAL_0: 5;
hence thesis by
Th318;
end;
theorem ::
XXREAL_1:344
p
<= q implies (
[.
-infty , q.]
\
[.p, q.[)
= (
[.
-infty , p.[
\/
{q})
proof
-infty
<= q by
XXREAL_0: 5;
hence thesis by
Th320;
end;
theorem ::
XXREAL_1:345
(
[.
-infty , q.]
\
].
-infty , s.[)
= (
{
-infty }
\/
[.s, q.])
proof
A1:
-infty
<= s by
XXREAL_0: 5;
-infty
<= q by
XXREAL_0: 5;
hence thesis by
A1,
Th322;
end;
theorem ::
XXREAL_1:346
(
[.
-infty , q.]
\
].
-infty , s.])
= (
{
-infty }
\/
].s, q.])
proof
A1:
-infty
<= s by
XXREAL_0: 5;
-infty
<= q by
XXREAL_0: 5;
hence thesis by
A1,
Th324;
end;
theorem ::
XXREAL_1:347
for q be
Real holds (
[.
-infty , q.[
\
].
-infty , s.[)
= (
{
-infty }
\/
[.s, q.[)
proof
let q be
Real;
A1: q
in
REAL by
XREAL_0:def 1;
-infty
<= s by
XXREAL_0: 5;
hence thesis by
A1,
Th321,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:348
for q be
Real holds (
[.
-infty , q.[
\
].
-infty , s.])
= (
{
-infty }
\/
].s, q.[)
proof
let q be
Real;
A1: q
in
REAL by
XREAL_0:def 1;
-infty
<= s by
XXREAL_0: 5;
hence thesis by
A1,
Th323,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:349
Th349: p
<= q implies (
].
-infty , q.[
\
{p})
= (
].
-infty , p.[
\/
].p, q.[)
proof
-infty
<= p by
XXREAL_0: 5;
hence thesis by
Th313;
end;
theorem ::
XXREAL_1:350
Th350: for p be
Real holds p
<= q implies (
].
-infty , q.]
\
{p})
= (
].
-infty , p.[
\/
].p, q.])
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th315,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:351
for q be
Real holds p
<= q implies (
].
-infty , q.]
\
].p, q.[)
= (
].
-infty , p.]
\/
{q})
proof
let q be
Real;
q
in
REAL by
XREAL_0:def 1;
hence thesis by
Th317,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:352
for q be
Real holds p
<= q implies (
].
-infty , q.]
\
[.p, q.[)
= (
].
-infty , p.[
\/
{q})
proof
let q be
Real;
q
in
REAL by
XREAL_0:def 1;
hence thesis by
Th319,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:353
r
< s implies (
].r,
+infty .]
\
].p, s.[)
= (
].r, p.]
\/
[.s,
+infty .]) by
Th299,
XXREAL_0: 3;
theorem ::
XXREAL_1:354
r
<= s implies (
[.r,
+infty .]
\
].p, s.[)
= (
[.r, p.]
\/
[.s,
+infty .])
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th300;
end;
theorem ::
XXREAL_1:355
r
< s implies (
].r,
+infty .[
\
[.p, s.[)
= (
].r, p.[
\/
[.s,
+infty .[) by
Th301,
XXREAL_0: 3;
theorem ::
XXREAL_1:356
r
<= s implies (
[.r,
+infty .[
\
[.p, s.[)
= (
[.r, p.[
\/
[.s,
+infty .[)
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th302;
end;
theorem ::
XXREAL_1:357
r
< s implies (
].r,
+infty .]
\
[.p, s.[)
= (
].r, p.[
\/
[.s,
+infty .]) by
Th303,
XXREAL_0: 3;
theorem ::
XXREAL_1:358
r
<= s implies (
[.r,
+infty .]
\
[.p, s.[)
= (
[.r, p.[
\/
[.s,
+infty .])
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th304;
end;
theorem ::
XXREAL_1:359
r
< s implies (
].r,
+infty .]
\
].p, s.])
= (
].r, p.]
\/
].s,
+infty .]) by
Th307,
XXREAL_0: 3;
theorem ::
XXREAL_1:360
r
<= s implies (
[.r,
+infty .]
\
].p, s.])
= (
[.r, p.]
\/
].s,
+infty .])
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th308;
end;
theorem ::
XXREAL_1:361
r
<= s implies (
].r,
+infty .[
\
[.p, s.])
= (
].r, p.[
\/
].s,
+infty .[)
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th309;
end;
theorem ::
XXREAL_1:362
r
<= s implies (
[.r,
+infty .[
\
[.p, s.])
= (
[.r, p.[
\/
].s,
+infty .[)
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th310;
end;
theorem ::
XXREAL_1:363
r
< s implies (
].r,
+infty .]
\
[.p, s.])
= (
].r, p.[
\/
].s,
+infty .]) by
Th311,
XXREAL_0: 3;
theorem ::
XXREAL_1:364
r
<= s implies (
[.r,
+infty .]
\
[.p, s.])
= (
[.r, p.[
\/
].s,
+infty .])
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th312;
end;
theorem ::
XXREAL_1:365
r
<= p implies (
].r,
+infty .[
\
{p})
= (
].r, p.[
\/
].p,
+infty .[)
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th313;
end;
theorem ::
XXREAL_1:366
r
<= p implies (
[.r,
+infty .[
\
{p})
= (
[.r, p.[
\/
].p,
+infty .[)
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th314;
end;
theorem ::
XXREAL_1:367
r
< p implies (
].r,
+infty .]
\
{p})
= (
].r, p.[
\/
].p,
+infty .]) by
Th315,
XXREAL_0: 3;
theorem ::
XXREAL_1:368
r
<= p implies (
[.r,
+infty .]
\
{p})
= (
[.r, p.[
\/
].p,
+infty .])
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th316;
end;
theorem ::
XXREAL_1:369
(
[.r,
+infty .]
\
].p,
+infty .[)
= (
[.r, p.]
\/
{
+infty })
proof
A1: r
<=
+infty by
XXREAL_0: 3;
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
A1,
Th318;
end;
theorem ::
XXREAL_1:370
(
[.r,
+infty .]
\
[.p,
+infty .[)
= (
[.r, p.[
\/
{
+infty })
proof
A1: r
<=
+infty by
XXREAL_0: 3;
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
A1,
Th320;
end;
theorem ::
XXREAL_1:371
for r be
Real holds (
].r,
+infty .]
\
].p,
+infty .[)
= (
].r, p.]
\/
{
+infty })
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
then r
<
+infty by
XXREAL_0: 9;
hence thesis by
Th317,
XXREAL_0: 3;
end;
theorem ::
XXREAL_1:372
for r be
Real holds (
].r,
+infty .]
\
[.p,
+infty .[)
= (
].r, p.[
\/
{
+infty })
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
then r
<
+infty by
XXREAL_0: 9;
hence thesis by
Th319,
XXREAL_0: 3;
end;
theorem ::
XXREAL_1:373
p
<= s implies (
[.p,
+infty .]
\
].p, s.[)
= (
{p}
\/
[.s,
+infty .])
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th322;
end;
theorem ::
XXREAL_1:374
p
<= s implies (
[.p,
+infty .]
\
].p, s.])
= (
{p}
\/
].s,
+infty .])
proof
p
<=
+infty by
XXREAL_0: 3;
hence thesis by
Th324;
end;
theorem ::
XXREAL_1:375
(
[.
-infty ,
+infty .]
\
].p, s.[)
= (
[.
-infty , p.]
\/
[.s,
+infty .]) by
Th326,
XXREAL_0: 3;
theorem ::
XXREAL_1:376
(
[.
-infty ,
+infty .[
\
[.p, s.[)
= (
[.
-infty , p.[
\/
[.s,
+infty .[) by
Th327,
XXREAL_0: 3;
theorem ::
XXREAL_1:377
(
[.
-infty ,
+infty .]
\
[.p, s.[)
= (
[.
-infty , p.[
\/
[.s,
+infty .]) by
Th328,
XXREAL_0: 3;
theorem ::
XXREAL_1:378
(
[.
-infty ,
+infty .]
\
].p, s.])
= (
[.
-infty , p.]
\/
].s,
+infty .]) by
Th330,
XXREAL_0: 3;
theorem ::
XXREAL_1:379
(
[.
-infty ,
+infty .[
\
[.p, s.])
= (
[.
-infty , p.[
\/
].s,
+infty .[) by
Th331,
XXREAL_0: 3;
theorem ::
XXREAL_1:380
(
[.
-infty ,
+infty .]
\
[.p, s.])
= (
[.
-infty , p.[
\/
].s,
+infty .]) by
Th332,
XXREAL_0: 3;
theorem ::
XXREAL_1:381
for s be
Real holds (
].
-infty ,
+infty .]
\
].p, s.[)
= (
].
-infty , p.]
\/
[.s,
+infty .]) by
Th334,
XXREAL_0: 3;
theorem ::
XXREAL_1:382
for s be
Real holds (
REAL
\
[.p, s.[)
= (
].
-infty , p.[
\/
[.s,
+infty .[) by
Th224,
Th335,
XXREAL_0: 3;
theorem ::
XXREAL_1:383
for s be
Real holds (
].
-infty ,
+infty .]
\
[.p, s.[)
= (
].
-infty , p.[
\/
[.s,
+infty .]) by
Th336,
XXREAL_0: 3;
theorem ::
XXREAL_1:384
for s be
Real holds (
].
-infty ,
+infty .]
\
].p, s.])
= (
].
-infty , p.]
\/
].s,
+infty .]) by
Th338,
XXREAL_0: 3;
theorem ::
XXREAL_1:385
(
REAL
\
[.p, s.])
= (
].
-infty , p.[
\/
].s,
+infty .[) by
Th224,
Th339,
XXREAL_0: 3;
theorem ::
XXREAL_1:386
for s be
Real holds (
].
-infty ,
+infty .]
\
[.p, s.])
= (
].
-infty , p.[
\/
].s,
+infty .]) by
Th340,
XXREAL_0: 3;
theorem ::
XXREAL_1:387
(
[.
-infty ,
+infty .[
\
{p})
= (
[.
-infty , p.[
\/
].p,
+infty .[) by
Th341,
XXREAL_0: 3;
theorem ::
XXREAL_1:388
(
[.
-infty ,
+infty .]
\
{p})
= (
[.
-infty , p.[
\/
].p,
+infty .]) by
Th342,
XXREAL_0: 3;
theorem ::
XXREAL_1:389
(
REAL
\
{p})
= (
].
-infty , p.[
\/
].p,
+infty .[) by
Th224,
Th349,
XXREAL_0: 3;
theorem ::
XXREAL_1:390
for p be
Real holds (
].
-infty ,
+infty .]
\
{p})
= (
].
-infty , p.[
\/
].p,
+infty .]) by
Th350,
XXREAL_0: 3;
theorem ::
XXREAL_1:391
for p be
Real holds r
< s implies (
].r,
+infty .[
\
].p, s.[)
= (
].r, p.]
\/
[.s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
then p
<
+infty by
XXREAL_0: 9;
hence thesis by
Th297;
end;
theorem ::
XXREAL_1:392
for p be
Real holds r
<= s implies (
[.r,
+infty .[
\
].p, s.[)
= (
[.r, p.]
\/
[.s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th298,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:393
for p be
Real holds r
< s implies (
].r,
+infty .[
\
].p, s.])
= (
].r, p.]
\/
].s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
then p
<
+infty by
XXREAL_0: 9;
hence thesis by
Th305;
end;
theorem ::
XXREAL_1:394
for p be
Real holds r
<= s implies (
[.r,
+infty .[
\
].p, s.])
= (
[.r, p.]
\/
].s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th306,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:395
for p be
Real holds p
<= s implies (
[.p,
+infty .[
\
].p, s.])
= (
{p}
\/
].s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th323,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:396
for p be
Real holds (
[.
-infty ,
+infty .[
\
].p, s.[)
= (
[.
-infty , p.]
\/
[.s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th325,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:397
for p be
Real holds (
[.
-infty ,
+infty .[
\
].p, s.])
= (
[.
-infty , p.]
\/
].s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th329,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:398
for s,p be
Real holds (
REAL
\
].p, s.[)
= (
].
-infty , p.]
\/
[.s,
+infty .[)
proof
let s,p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th224,
Th333,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:399
for s,p be
Real holds (
REAL
\
].p, s.])
= (
].
-infty , p.]
\/
].s,
+infty .[)
proof
let s,p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th224,
Th337,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:400
for p be
Real holds p
<= s implies (
[.p,
+infty .[
\
].p, s.[)
= (
{p}
\/
[.s,
+infty .[)
proof
let p be
Real;
p
in
REAL by
XREAL_0:def 1;
hence thesis by
Th321,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:401
Th401: r
< s implies (
[.r, s.]
\
[.r, s.[)
=
{s}
proof
[.s, s.]
=
{s} by
Th17;
hence thesis by
Th184;
end;
theorem ::
XXREAL_1:402
Th402: r
< s implies (
].r, s.]
\
].r, s.[)
=
{s}
proof
[.s, s.]
=
{s} by
Th17;
hence thesis by
Th188;
end;
theorem ::
XXREAL_1:403
Th403: r
< t implies (
[.r, t.]
\
].r, t.])
=
{r}
proof
[.r, r.]
=
{r} by
Th17;
hence thesis by
Th192;
end;
theorem ::
XXREAL_1:404
Th404: r
< t implies (
[.r, t.[
\
].r, t.[)
=
{r}
proof
[.r, r.]
=
{r} by
Th17;
hence thesis by
Th196;
end;
theorem ::
XXREAL_1:405
for s be
Real holds (
[.
-infty , s.]
\
[.
-infty , s.[)
=
{s}
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th401,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:406
for s be
Real holds (
].
-infty , s.]
\
].
-infty , s.[)
=
{s}
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th402,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:407
for s be
Real holds (
[.
-infty , s.]
\
].
-infty , s.])
=
{
-infty }
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th403,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:408
for s be
Real holds (
[.
-infty , s.[
\
].
-infty , s.[)
=
{
-infty }
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th404,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:409
for s be
Real holds (
[.s,
+infty .]
\
[.s,
+infty .[)
=
{
+infty }
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th401,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:410
for s be
Real holds (
].s,
+infty .]
\
].s,
+infty .[)
=
{
+infty }
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th402,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:411
for s be
Real holds (
[.s,
+infty .]
\
].s,
+infty .])
=
{s}
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th403,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:412
for s be
Real holds (
[.s,
+infty .[
\
].s,
+infty .[)
=
{s}
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th404,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:413
r
<= s & s
< t implies (
[.r, s.]
\/
[.s, t.[)
=
[.r, t.[
proof
assume that
A1: r
<= s and
A2: s
< t;
let p;
thus p
in (
[.r, s.]
\/
[.s, t.[) implies p
in
[.r, t.[
proof
assume p
in (
[.r, s.]
\/
[.s, t.[);
then p
in
[.r, s.] or p
in
[.s, t.[ by
XBOOLE_0:def 3;
then
A3: r
<= p & p
<= s or s
<= p & p
< t by
Th1,
Th3;
then
A4: r
<= p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th3;
end;
assume p
in
[.r, t.[;
then r
<= p & p
<= s or s
<= p & p
< t by
Th3;
then p
in
[.r, s.] or p
in
[.s, t.[ by
Th1,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:414
r
< s & s
<= t implies (
].r, s.]
\/
[.s, t.])
=
].r, t.]
proof
assume that
A1: r
< s and
A2: s
<= t;
let p;
thus p
in (
].r, s.]
\/
[.s, t.]) implies p
in
].r, t.]
proof
assume p
in (
].r, s.]
\/
[.s, t.]);
then p
in
].r, s.] or p
in
[.s, t.] by
XBOOLE_0:def 3;
then
A3: r
< p & p
<= s or s
<= p & p
<= t by
Th1,
Th2;
then
A4: r
< p by
A1,
XXREAL_0: 2;
p
<= t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th2;
end;
assume p
in
].r, t.];
then r
< p & p
<= s or s
<= p & p
<= t by
Th2;
then p
in
].r, s.] or p
in
[.s, t.] by
Th1,
Th2;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:415
r
< s & s
< t implies (
].r, s.]
\/
[.s, t.[)
=
].r, t.[
proof
assume that
A1: r
< s and
A2: s
< t;
let p;
thus p
in (
].r, s.]
\/
[.s, t.[) implies p
in
].r, t.[
proof
assume p
in (
].r, s.]
\/
[.s, t.[);
then p
in
].r, s.] or p
in
[.s, t.[ by
XBOOLE_0:def 3;
then
A3: r
< p & p
<= s or s
<= p & p
< t by
Th2,
Th3;
then
A4: r
< p by
A1,
XXREAL_0: 2;
p
< t by
A2,
A3,
XXREAL_0: 2;
hence thesis by
A4,
Th4;
end;
assume p
in
].r, t.[;
then r
< p & p
<= s or s
<= p & p
< t by
Th4;
then p
in
].r, s.] or p
in
[.s, t.[ by
Th2,
Th3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
XXREAL_1:416
r
<= s & s
< t implies (
[.r, s.]
/\
[.s, t.[)
=
{s}
proof
assume that
A1: r
<= s and
A2: s
< t;
now
let x be
object;
hereby
assume
A3: x
in (
[.r, s.]
/\
[.s, t.[);
then
reconsider p = x as
ExtReal;
A4: p
in
[.r, s.] by
A3,
XBOOLE_0:def 4;
p
in
[.s, t.[ by
A3,
XBOOLE_0:def 4;
then
A5: s
<= p by
Th3;
p
<= s by
A4,
Th1;
hence x
= s by
A5,
XXREAL_0: 1;
end;
assume
A6: x
= s;
A7: s
in
[.r, s.] by
A1,
Th1;
s
in
[.s, t.[ by
A2,
Th3;
hence x
in (
[.r, s.]
/\
[.s, t.[) by
A6,
A7,
XBOOLE_0:def 4;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
XXREAL_1:417
r
< s & s
<= t implies (
].r, s.]
/\
[.s, t.])
=
{s}
proof
assume that
A1: r
< s and
A2: s
<= t;
now
let x be
object;
hereby
assume
A3: x
in (
].r, s.]
/\
[.s, t.]);
then
reconsider p = x as
ExtReal;
A4: p
in
].r, s.] by
A3,
XBOOLE_0:def 4;
p
in
[.s, t.] by
A3,
XBOOLE_0:def 4;
then
A5: s
<= p by
Th1;
p
<= s by
A4,
Th2;
hence x
= s by
A5,
XXREAL_0: 1;
end;
assume
A6: x
= s;
A7: s
in
].r, s.] by
A1,
Th2;
s
in
[.s, t.] by
A2,
Th1;
hence x
in (
].r, s.]
/\
[.s, t.]) by
A6,
A7,
XBOOLE_0:def 4;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
XXREAL_1:418
r
<= s & s
<= t implies (
[.r, s.]
/\
[.s, t.])
=
{s}
proof
assume that
A1: r
<= s and
A2: s
<= t;
now
let x be
object;
hereby
assume
A3: x
in (
[.r, s.]
/\
[.s, t.]);
then
reconsider p = x as
ExtReal;
A4: p
in
[.r, s.] by
A3,
XBOOLE_0:def 4;
p
in
[.s, t.] by
A3,
XBOOLE_0:def 4;
then
A5: s
<= p by
Th1;
p
<= s by
A4,
Th1;
hence x
= s by
A5,
XXREAL_0: 1;
end;
assume
A6: x
= s;
A7: s
in
[.r, s.] by
A1,
Th1;
s
in
[.s, t.] by
A2,
Th1;
hence x
in (
[.r, s.]
/\
[.s, t.]) by
A6,
A7,
XBOOLE_0:def 4;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
XXREAL_1:419
[.
-infty , s.]
= (
].
-infty , s.[
\/
{
-infty , s}) by
Th128,
XXREAL_0: 5;
theorem ::
XXREAL_1:420
[.
-infty , s.]
= (
[.
-infty , s.[
\/
{s}) by
Th129,
XXREAL_0: 5;
theorem ::
XXREAL_1:421
[.
-infty , s.]
= (
{
-infty }
\/
].
-infty , s.]) by
Th130,
XXREAL_0: 5;
theorem ::
XXREAL_1:422
for s be
Real holds
[.
-infty , s.[
= (
{
-infty }
\/
].
-infty , s.[)
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th131,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:423
for s be
Real holds
].
-infty , s.]
= (
].
-infty , s.[
\/
{s})
proof
let s be
Real;
s
in
REAL by
XREAL_0:def 1;
hence thesis by
Th132,
XXREAL_0: 12;
end;
theorem ::
XXREAL_1:424
[.r,
+infty .]
= (
].r,
+infty .[
\/
{r,
+infty }) by
Th128,
XXREAL_0: 3;
theorem ::
XXREAL_1:425
[.r,
+infty .]
= (
[.r,
+infty .[
\/
{
+infty }) by
Th129,
XXREAL_0: 3;
theorem ::
XXREAL_1:426
[.r,
+infty .]
= (
{r}
\/
].r,
+infty .]) by
Th130,
XXREAL_0: 3;
theorem ::
XXREAL_1:427
for r be
Real holds
[.r,
+infty .[
= (
{r}
\/
].r,
+infty .[)
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
hence thesis by
Th131,
XXREAL_0: 9;
end;
theorem ::
XXREAL_1:428
for r be
Real holds
].r,
+infty .]
= (
].r,
+infty .[
\/
{
+infty })
proof
let r be
Real;
r
in
REAL by
XREAL_0:def 1;
hence thesis by
Th132,
XXREAL_0: 9;
end;