Copyright (c) 1993 Association of Mizar Users
environ
vocabulary SUPINF_1, ARYTM_3, RLVECT_1, ARYTM_1, ORDINAL2, RCOMP_1, BOOLE,
MEASURE5, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, REAL_1, SUPINF_1,
SUPINF_2;
constructors REAL_1, SUPINF_2, MEMBERED, XBOOLE_0;
clusters SUBSET_1, XREAL_0, XBOOLE_0, MEMBERED, ZFMISC_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, SUPINF_1, SUPINF_2, REAL_1, MEASURE3, MEASURE4, XREAL_0,
XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes SUPINF_1;
begin :: Some theorems about R_eal numbers
reserve x,y,a,b,a1,b1,a2,b2 for R_eal;
theorem Th1:
x <> -infty & x <> +infty & x <=' y implies
0. <=' y - x
proof
assume
A1:x <> -infty & x <> +infty & x <=' y;
consider z being R_eal such that
A2:z = 0.;
z + x = x by A2,SUPINF_2:18;
hence thesis by A1,A2,MEASURE4:2;
end;
theorem Th2:
(not (x = -infty & y = -infty) & not (x = +infty & y = +infty) & x <=' y)
implies 0. <=' y - x
proof
assume
A1:not (x = -infty & y = -infty) & not (x = +infty & y = +infty) & x <=' y;
A2: (x in REAL or x in {-infty,+infty}) & (y in REAL or y in {-infty,+infty})
by SUPINF_1:def 6,XBOOLE_0:def 2;
per cases by A1,A2,TARSKI:def 2;
suppose x in REAL & y in REAL;
then not x = -infty & not x = +infty by SUPINF_1:31;
hence thesis by A1,Th1;
suppose x in REAL & y = -infty;
hence thesis by A1,SUPINF_1:23;
suppose x in REAL & y = +infty;
hence thesis by SUPINF_1:2,SUPINF_2:6,19;
suppose x = -infty & y in REAL;
hence thesis by SUPINF_1:6,SUPINF_2:7,19;
suppose x = -infty & y = +infty;
hence thesis by SUPINF_2:7,19;
suppose x = +infty & y in REAL; hence thesis by A1,SUPINF_1:24;
suppose x = +infty & y = -infty; hence thesis by A1,SUPINF_1:24;
end;
canceled 5;
theorem
for a,b,c being R_eal holds
(b <> -infty & b <> +infty &
not (a = -infty & c = -infty) & not (a = +infty & c = +infty)) implies
(c - b) + (b - a) = c - a
proof
let a,b,c be R_eal;
assume
A1:b <> -infty & b <> +infty &
not (a = -infty & c = -infty) & not (a = +infty & c = +infty);
A2:(a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
per cases by A1,A2,TARSKI:def 2;
suppose
A3:a in REAL & b in REAL;
A4: c in REAL or c in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
now per cases by A3,A4,TARSKI:def 2;
suppose a in REAL & b in REAL & c in REAL;
then consider x,y,z being Real such that
A5:x = a & y = b & z = c;
c - b = z - y & b - a = y - x by A5,SUPINF_2:5;
hence (c -b) + (b - a) = (z - y) + (y - x) by SUPINF_2:1
.= z - (y - (y - x)) by XCMPLX_1:37
.= z - (y - y + x) by XCMPLX_1:37
.= z - (y + (-y) + x) by XCMPLX_0:def 8
.= z - (0 + x) by XCMPLX_0:def 6
.= c - a by A5,SUPINF_2:5;
suppose
A6:a in REAL & b in REAL & c = -infty;
then A7:(c -b) + (b - a) = -infty
+ (b - a) by SUPINF_1:6,SUPINF_2:7;
consider x,y being Real such that
A8:x = a & y = b by A6;
b - a = y - x by A8,SUPINF_2:5;
then not b - a = +infty by SUPINF_1:2;
then (c -b) + (b - a) = -infty by A7,SUPINF_2:def 2;
hence thesis by A6,SUPINF_1:6,SUPINF_2:7;
suppose
A9:a in REAL & b in REAL & c = +infty;
then A10:(c -b) + (b - a) = +infty
+ (b - a) by SUPINF_1:2,SUPINF_2:6;
consider x,y being Real such that
A11:x = a & y = b by A9;
b - a = y - x by A11,SUPINF_2:5;
then not b - a = -infty by SUPINF_1:6;
then (c -b) + (b - a) = +infty by A10,SUPINF_2:def 2;
hence thesis by A9,SUPINF_1:2,SUPINF_2:6;
end;
hence thesis;
suppose
A12:a = -infty & b in REAL;
A13: c in REAL or c in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
now per cases by A1,A12,A13,TARSKI:def 2;
suppose
A14:a = -infty & b in REAL & c in REAL;
then A15:(c -b) + (b - a) = (c - b) + (+infty) by SUPINF_1:6,
SUPINF_2:7;
consider x,y being Real such that
A16:x = c & y = b by A14;
c - b = x - y by A16,SUPINF_2:5;
then not c - b = -infty by SUPINF_1:6;
then (c -b) + (b - a) = +infty by A15,SUPINF_2:def 2;
hence thesis by A14,SUPINF_1:6,SUPINF_2:7;
suppose
A17:a = -infty & b in REAL & c = +infty;
then A18:(c -b) + (b - a) = (c - b) + (+infty) by SUPINF_1:6,
SUPINF_2:7;
c - b = +infty by A17,SUPINF_1:2,SUPINF_2:6;
then (c -b) + (b - a) = +infty by A18,SUPINF_1:14,SUPINF_2:def 2
;
hence thesis by A17,SUPINF_1:14,SUPINF_2:7;
end;
hence thesis;
suppose
A19:a = +infty & b in REAL;
A20: c in REAL or c in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
now per cases by A1,A19,A20,TARSKI:def 2;
suppose
A21:a = +infty & b in REAL & c in REAL;
then A22: (c -b) + (b - a) = (c - b) + (-infty) by SUPINF_1:2,SUPINF_2:6
;
consider x,y being Real such that
A23:x = c & y = b by A21;
c - b = x - y by A23,SUPINF_2:5;
then not c - b = +infty by SUPINF_1:2;
then (c -b) + (b - a) = -infty by A22,SUPINF_2:def 2;
hence thesis by A21,SUPINF_1:2,SUPINF_2:6;
suppose
A24:a = +infty & b in REAL & c = -infty;
then A25:(c -b) + (b - a) = (c - b) + (-infty) by SUPINF_1:2,
SUPINF_2:6;
c - b = -infty by A24,SUPINF_1:6,SUPINF_2:7;
then (c -b) + (b - a) = -infty by A25,SUPINF_1:14,SUPINF_2:def 2
;
hence thesis by A24,SUPINF_1:14,SUPINF_2:6;
end;
hence thesis;
end;
theorem
inf{a1,a2} <=' a1 & inf{a1,a2} <=' a2 &
a1 <=' sup{a1,a2} & a2 <=' sup{a1,a2}
proof
a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
hence thesis by SUPINF_1:76,79;
end;
:: PROPERTIES OF THE INTERVALS
RSetEq {P[set]} : for X1,X2 being Subset of REAL st
(for x being R_eal holds x in X1 iff P[x]) &
(for x being R_eal holds x in X2 iff P[x]) holds X1 = X2
proof
let A1,A2 be Subset of REAL such that
A1:for x being R_eal holds x in A1 iff P[x] and
A2:for x being R_eal holds x in A2 iff P[x];
thus A1 c= A2
proof
let x be set;
assume
A3:x in A1;
then x in REAL;
then reconsider x as R_eal;
P[x] by A1,A3;
hence thesis by A2;
end;
let x be set;
assume
A4:x in A2;
then x in REAL;
then reconsider x as R_eal;
P[x] by A2,A4;
hence thesis by A1;
end;
definition let a,b be R_eal;
defpred P[R_eal] means a <=' $1 & $1 <=' b & $1 in REAL;
func [.a,b.] -> Subset of REAL means
:Def1:for x being R_eal holds
x in it iff a <=' x & x <=' b & x in REAL;
existence
proof
consider A being Subset of REAL \/ {-infty,+infty} such that
A1:for x being R_eal holds x in A iff P[x] from SepR_eal;
for x being set holds x in A implies x in REAL by A1,SUPINF_1:def 6;
then reconsider A as Subset of REAL by TARSKI:def 3;
take A;
thus thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being Subset of REAL st
(for x being R_eal holds x in X1 iff P[x]) &
(for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
end;
defpred P[R_eal] means a <' $1 & $1 <' b & $1 in REAL;
func ].a,b.[ -> Subset of REAL means
:Def2:for x being R_eal holds
x in it iff (a <' x & x <' b & x in REAL);
existence
proof
consider A being Subset of REAL \/ {-infty,+infty} such that
A2:for x being R_eal holds x in A iff P[x] from SepR_eal;
for x being set holds x in A implies x in REAL by A2,SUPINF_1:def 6;
then reconsider A as Subset of REAL by TARSKI:def 3;
take A;
thus thesis by A2;
end;
uniqueness
proof
thus for X1,X2 being Subset of REAL st
(for x being R_eal holds x in X1 iff P[x]) &
(for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
end;
defpred P[R_eal] means a <' $1 & $1 <=' b & $1 in REAL;
func ].a,b.] -> Subset of REAL means
:Def3:for x being R_eal holds
x in it iff (a <' x & x <=' b & x in REAL);
existence
proof
consider A being Subset of REAL \/ {-infty,+infty} such that
A3:for x being R_eal holds x in A iff P[x] from SepR_eal;
for x being set holds x in A implies x in REAL by A3,SUPINF_1:def 6;
then reconsider A as Subset of REAL by TARSKI:def 3;
take A;
thus thesis by A3;
end;
uniqueness
proof
thus for X1,X2 being Subset of REAL st
(for x being R_eal holds x in X1 iff P[x]) &
(for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
end;
defpred P[R_eal] means a <=' $1 & $1 <' b & $1 in REAL;
func [.a,b.[ -> Subset of REAL means
:Def4:for x being R_eal holds
x in it iff (a <=' x & x <' b & x in REAL);
existence
proof
consider A being Subset of REAL \/ {-infty,+infty} such that
A4:for x being R_eal holds x in A iff P[x] from SepR_eal;
for x being set holds x in A implies x in REAL by A4,SUPINF_1:def 6;
then reconsider A as Subset of REAL by TARSKI:def 3;
take A;
thus thesis by A4;
end;
uniqueness
proof
thus for X1,X2 being Subset of REAL st
(for x being R_eal holds x in X1 iff P[x]) &
(for x being R_eal holds x in X2 iff P[x]) holds X1 = X2 from RSetEq;
end;
end;
definition let IT be Subset of REAL;
attr IT is open_interval means
:Def5: ex a,b being R_eal st a <=' b & IT = ].a,b.[;
attr IT is closed_interval means
:Def6:ex a,b being R_eal st a <=' b & IT = [.a,b.];
end;
definition
cluster open_interval Subset of REAL;
existence
proof
consider a,b being R_eal such that
A1:a = -infty & b = +infty;
take ].a,b.[, a,b;
thus thesis by A1,SUPINF_1:20;
end;
cluster closed_interval Subset of REAL;
existence
proof
consider a,b being R_eal such that
A2:a = -infty & b = +infty;
take [.a,b.],a,b;
thus thesis by A2,SUPINF_1:20;
end;
end;
definition let IT be Subset of REAL;
attr IT is right_open_interval means
:Def7: ex a,b being R_eal st a <=' b & IT = [.a,b.[;
synonym IT is left_closed_interval;
end;
definition let IT be Subset of REAL;
attr IT is left_open_interval means
:Def8:ex a,b being R_eal st a <=' b & IT = ].a,b.];
synonym IT is right_closed_interval;
end;
definition
cluster right_open_interval Subset of REAL;
existence
proof
consider a,b being R_eal such that
A1:a = -infty & b = +infty;
take [.a,b.[,a,b;
thus thesis by A1,SUPINF_1:20;
end;
cluster left_open_interval Subset of REAL;
existence
proof
consider a,b being R_eal such that
A2:a = -infty & b = +infty;
take ].a,b.],a,b;
thus thesis by A2,SUPINF_1:20;
end;
end;
definition let IT be Subset of REAL;
attr IT is interval means
:Def9:IT is open_interval or IT is closed_interval or
IT is right_open_interval or IT is left_open_interval;
end;
definition
cluster interval Subset of REAL;
existence
proof
consider I being open_interval Subset of REAL;
take I;
thus I is open_interval or I is closed_interval
or I is right_open_interval or I is left_open_interval;
end;
end;
definition
mode Interval is interval Subset of REAL;
end;
reserve A,B for Interval;
definition
cluster open_interval -> interval Subset of REAL;
coherence by Def9;
cluster closed_interval -> interval Subset of REAL;
coherence by Def9;
cluster right_open_interval -> interval Subset of REAL;
coherence by Def9;
cluster left_open_interval -> interval Subset of REAL;
coherence by Def9;
end;
canceled;
theorem Th11:
for x being set,
a,b being R_eal st
(x in ].a,b.[ or x in [.a,b.] or x in [.a,b.[ or x in ].a,b.]) holds
x is R_eal
proof
let x be set,
a,b be R_eal;
assume x in ].a,b.[ or x in [.a,b.] or x in [.a,b.[ or x in ].a,b.];
then x in REAL;
hence thesis;
end;
theorem Th12:
for a,b being R_eal st b <' a holds
].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {}
proof
let a,b be R_eal;
assume
A1:b <' a;
thus ].a,b.[ = {}
proof assume
A2: not thesis;
consider x being Element of ].a,b.[;
reconsider x as R_eal by A2,Th11;
b <=' a & b <> a & a <=' x & x <=' b by A1,A2,Def2;
then b <=' a & b <> a & a <=' b by SUPINF_1:29;
hence thesis by SUPINF_1:22;
end;
thus [.a,b.] = {}
proof assume
A3: not thesis;
consider x being Element of [.a,b.];
reconsider x as R_eal by A3,Th11;
b <=' a & b <> a & a <=' x & x <=' b by A1,A3,Def1;
then b <=' a & b <> a & a <=' b by SUPINF_1:29;
hence thesis by SUPINF_1:22;
end;
thus [.a,b.[ = {}
proof assume
A4: not thesis;
consider x being Element of [.a,b.[;
reconsider x as R_eal by A4,Th11;
b <=' a & b <> a & a <=' x & x <=' b by A1,A4,Def4;
then b <=' a & b <> a & a <=' b by SUPINF_1:29;
hence thesis by SUPINF_1:22;
end;
assume
A5: not thesis;
consider x being Element of ].a,b.];
reconsider x as R_eal by A5,Th11;
b <=' a & b <> a & a <=' x & x <=' b by A1,A5,Def3;
then b <=' a & b <> a & a <=' b by SUPINF_1:29;
hence thesis by SUPINF_1:22;
end;
theorem Th13:
for a being R_eal holds
].a,a.[ = {} & [.a,a.[ = {} & ].a,a.] = {}
proof
let a be R_eal;
thus ].a,a.[ = {}
proof assume
A1: not thesis;
consider x being Element of ].a,a.[;
reconsider x as R_eal by A1,Th11;
a <=' x & x <=' a & x <> a by A1,Def2;
hence thesis by SUPINF_1:22;
end;
thus [.a,a.[ = {}
proof assume
A2: not thesis;
consider x being Element of [.a,a.[;
reconsider x as R_eal by A2,Th11;
a <=' x & x <=' a & x <> a by A2,Def4;
hence thesis by SUPINF_1:22;
end;
assume
A3:not thesis;
consider x being Element of ].a,a.];
reconsider x as R_eal by A3,Th11;
a <=' x & x <=' a & x <> a by A3,Def3;
hence thesis by SUPINF_1:22;
end;
theorem Th14:
for a being R_eal holds
((a = -infty or a = +infty) implies [.a,a.] = {}) &
((a <> -infty & a <> +infty) implies [.a,a.] = {a})
proof
let a be R_eal;
thus (a = -infty or a = +infty) implies [.a,a.] = {}
proof
assume
A1:a = -infty or a = +infty;
assume
A2: not thesis;
per cases by A1;
suppose
A3:a = -infty;
consider x being Element of [.a,a.];
reconsider x as R_eal by A2,Th11;
a <=' x & x <=' a & x in REAL by A2,Def1;
hence thesis by A3,SUPINF_1:6,22;
suppose
A4:a = +infty;
consider x being Element of [.a,a.];
reconsider x as R_eal by A2,Th11;
a <=' x & x <=' a & x in REAL by A2,Def1;
hence thesis by A4,SUPINF_1:2,22;
end;
assume
A5:a <> -infty & a <> +infty;
for x being set holds x in [.a,a.] iff x = a
proof
let x be set;
hereby assume
A6:x in [.a,a.];
then reconsider x' = x as R_eal by Th11;
a <=' x' & x' <=' a & x in REAL by A6,Def1;
hence x = a by SUPINF_1:22;
end;
assume
A7:x = a;
then reconsider x as R_eal;
x is Real by A5,A7,MEASURE3:2;
hence thesis by A7,Def1;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th15:
for a,b being R_eal st b <=' a holds
].a,b.[ = {} & [.a,b.[ = {} & ].a,b.] = {} &
[.a,b.] c= {a} & [.a,b.] c= {b}
proof
let a,b be R_eal;
assume
A1:b <=' a;
thus ].a,b.[ = {} & [.a,b.[ = {} & ].a,b.] = {}
proof
per cases;
suppose b <> a; then b <' a by A1,SUPINF_1:22;hence thesis by Th12;
suppose b = a;hence thesis by Th13;
end;
thus [.a,b.] c= {a}
proof
per cases;
suppose b <> a; then b <' a by A1,SUPINF_1:22;
then [.a,b.] = {} by Th12;
hence thesis by XBOOLE_1:2;
suppose
A2:b = a;
thus [.a,b.] c= {a}
proof
per cases;
suppose a = -infty or a = +infty;
then [.a,b.] = {} by A2,Th14;
hence thesis by XBOOLE_1:2;
suppose a <> -infty & a <> +infty;
hence thesis by A2,Th14;
end;
end;
per cases;
suppose b <> a; then b <' a by A1,SUPINF_1:22;
then [.a,b.] = {} by Th12;
hence thesis by XBOOLE_1:2;
suppose
A3:b = a;
thus [.a,b.] c= {b}
proof
per cases;
suppose b = -infty or b = +infty;
then [.a,b.] = {} by A3,Th14;
hence thesis by XBOOLE_1:2;
suppose b <> -infty & b <> +infty; hence thesis by A3,Th14;
end;
end;
theorem
for a,b,c being R_eal st a <' b & b <' c holds b in REAL
proof
let a,b,c be R_eal;
assume
A1:a <' b & b <' c;
then A2:b <> -infty by SUPINF_1:21;
b <> +infty by A1,SUPINF_1:20;
then b is Real by A2,MEASURE3:2;
hence thesis;
end;
theorem Th17:
for a,b being R_eal st a <' b
ex x being R_eal st a <' x & x <' b & x in REAL
proof
let a,b be R_eal;
assume
A1:a <' b;
A2:(a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty})
by SUPINF_1:def 6,XBOOLE_0:def 2;
A3: not a = +infty & not b = -infty
proof
assume a = +infty or b = -infty;
hence thesis by A1,SUPINF_1:23,24;
end;
per cases by A2,A3,TARSKI:def 2;
suppose a in REAL & b in REAL;
then consider x,y being Real such that
A4:x = a & y = b & x<=y by A1,SUPINF_1:16;
x<y by A1,A4,REAL_1:def 5;
then consider z being real number such that
A5:x<z & z<y by REAL_1:75;
reconsider z as Real by XREAL_0:def 1;
reconsider o = z as R_eal by SUPINF_1:10;
take o;
o in REAL & a <=' o & o <=' b & a <> o & o <> b
by A4,A5,SUPINF_1:def 7;
hence thesis by SUPINF_1:22;
suppose
A6:a in REAL & b = +infty;
then reconsider x = a as Real;
consider z being real number such that
A7:x<z by REAL_1:76;
reconsider z as Real by XREAL_0:def 1;
reconsider o = z as R_eal by SUPINF_1:10;
take o;
o in REAL & a <=' o & a <> o by A7,SUPINF_1:def 7;
hence thesis by A6,SUPINF_1:22,31;
suppose
A8:a = -infty & b in REAL;
then reconsider y = b as Real;
consider z being real number such that
A9:z<y by REAL_1:77;
reconsider z as Real by XREAL_0:def 1;
reconsider o = z as R_eal by SUPINF_1:10;
take o;
o in REAL & o <=' b & o <> b by A9,SUPINF_1:def 7;
hence thesis by A8,SUPINF_1:22,31;
suppose
A10:a = -infty & b = +infty;
take 0.;
thus thesis by A10,SUPINF_1:31,SUPINF_2:def 1;
end;
theorem Th18:
for a,b,c being R_eal st a <' b & a <' c
ex x being R_eal st a <' x & x <' b & x <' c & x in REAL
proof
let a,b,c be R_eal;
assume
A1:a <' b & a <' c;
b <=' c or c <=' b;
then a <' inf{b,c} by A1,SUPINF_1:96;
then consider x being R_eal such that
A2:a <' x & x <' inf{b,c} & x in REAL by Th17;
ex o being R_eal st o in {b,c} & o <=' b
proof
take b;
thus thesis by TARSKI:def 2;
end;
then A3:inf{b,c} <=' b by SUPINF_1:98;
ex o being R_eal st (o in {b,c} & o <=' c)
proof
take c;
thus thesis by TARSKI:def 2;
end;
then A4:inf{b,c} <=' c by SUPINF_1:98;
take x;
thus thesis by A2,A3,A4,SUPINF_1:29;
end;
theorem Th19:
for a,b,c being R_eal st a <' c & b <' c
ex x being R_eal st a <' x & b <' x & x <' c & x in REAL
proof
let a,b,c be R_eal;
assume
A1:a <' c & b <' c;
a <=' b or b <=' a;
then sup{a,b} <' c by A1,SUPINF_1:93;
then consider x being R_eal such that
A2:sup{a,b} <' x & x <' c & x in REAL by Th17;
take x;
a in {a,b} & b in {a,b} by TARSKI:def 2;
hence thesis by A2,SUPINF_1:97;
end;
theorem Th20:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ & not x in ].a2,b2.[) or
(not x in ].a1,b1.[ & x in ].a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.[) or (not x in ].a1,b1.[ & x in ].a2,b2.[))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in ].a1,b1.[ by A3,Def2;
not x in ].a2,b2.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1;hence thesis by A2;
suppose
a2 <' b2;
then consider x being R_eal such that
A5:a2 <' x & x <' b2 & x in REAL by Th17;
now per cases;
suppose a1 <' b1;hence thesis by A2;
suppose b1 <=' a1;
then not x in ].a1,b1.[ & x in ].a2,b2.[ by A5,Def2,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th21:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.[) or (not x in ].a1,b1.[ & x in ].a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.[) or (not x in ].a1,b1.[ & x in ].a2,b2.[))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in ].a2,b2.[ by A3,Def2;
not x in ].a1,b1.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2;hence thesis by A2;
suppose
A6: b2 <=' a2;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in ].a1,b1.[ & not x in].a2,b2.[ by A6,A7,Def2,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th22:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in [.a1,b1.] by A3,Def1;
not x in ].a2,b2.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose a2 <' b2;
then consider x being R_eal such that
A5:a2 <' x & x <' b2 & x in REAL by Th17;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: [.a1,b1.] c= {a1} by Th15;
A7:x in ].a2,b2.[ by A5,Def2;
not x in [.a1,b1.] by A1,A5,A6,TARSKI:def 1;
hence thesis by A7;
end;
hence thesis;
end;
theorem Th23:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] & x in ].a2,b2.[))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in ].a2,b2.[ by A3,Def2;
not x in [.a1,b1.] by A3,Def1;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2; hence thesis by A2;
suppose
A6: b2 <=' a2;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in [.a1,b1.] & not x in].a2,b2.[ by A6,A7,Def1,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th24:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in ].a1,b1.[ by A3,Def2;
not x in [.a2,b2.] by A3,Def1;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: ].a1,b1.[ = {} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
x in [.a2,b2.] by A7,Def1;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th25:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.]) or (not x in ].a1,b1.[ & x in [.a2,b2.]))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in [.a2,b2.] by A3,Def1;
not x in ].a1,b1.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2; hence thesis by A2;
suppose b2 <=' a2;
then A6: [.a2,b2.] c= {b2} by Th15;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
A8:x in ].a1,b1.[ by A7,Def2;
not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
hence thesis by A8;
end;
hence thesis;
end;
theorem Th26:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in ].a1,b1.[ by A3,Def2;
not x in [.a2,b2.[ by A3,Def4;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: ].a1,b1.[ = {} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
x in [.a2,b2.[ by A7,Def4;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th27:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ & x in [.a2,b2.[))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in [.a2,b2.[ by A3,Def4;
not x in ].a1,b1.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2; hence thesis by A2;
suppose b2 <=' a2;
then A6: [.a2,b2.[ = {} by Th15;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in ].a1,b1.[ by A7,Def2;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th28:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in [.a1,b1.[ by A3,Def4;
not x in ].a2,b2.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: [.a1,b1.[ = {} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
x in ].a2,b2.[ by A7,Def2;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th29:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.[) or (not x in [.a1,b1.[ & x in ].a2,b2.[))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in ].a2,b2.[ by A3,Def2;
not x in [.a1,b1.[ by A3,Def4;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2; hence thesis by A2;
suppose
A6: b2 <=' a2;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in [.a1,b1.[ & not x in].a2,b2.[ by A6,A7,Def4,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th30:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in ].a1,b1.[ by A3,Def2;
not x in ].a2,b2.] by A3,Def3;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: ].a1,b1.[ = {} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
x in ].a2,b2.] by A7,Def3;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th31:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ & x in ].a2,b2.]))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in ].a2,b2.] by A3,Def3;
not x in ].a1,b1.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2; hence thesis by A2;
suppose b2 <=' a2;
then A6: ].a2,b2.] = {} by Th15;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in ].a1,b1.[ by A7,Def2;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th32:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in ].a1,b1.] by A3,Def3;
not x in ].a2,b2.[ by A3,Def2;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: ].a1,b1.] = {} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
x in ].a2,b2.[ by A7,Def2;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th33:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.[) or (not x in ].a1,b1.] & x in ].a2,b2.[))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in ].a2,b2.[ by A3,Def2;
not x in ].a1,b1.] by A3,Def3;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2;
hence thesis by A2;
suppose
A6: b2 <=' a2;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in ].a1,b1.] & not x in].a2,b2.[ by A6,A7,Def3,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th34:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in [.a1,b1.] by A3,Def1;
not x in [.a2,b2.] by A3,Def1;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: [.a1,b1.] c= {a1} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
A8:x in [.a2,b2.] by A7,Def1;
not x in [.a1,b1.] by A1,A6,A7,TARSKI:def 1;
hence thesis by A8;
end;
hence thesis;
end;
theorem Th35:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] & x in [.a2,b2.]))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in [.a2,b2.] by A3,Def1;
not x in [.a1,b1.] by A3,Def1;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2;
hence thesis by A2;
suppose b2 <=' a2;
then A6: [.a2,b2.] c= {b2} by Th15;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
A8:x in [.a1,b1.] by A7,Def1;
not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
hence thesis by A8;
end;
hence thesis;
end;
theorem Th36:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in [.a1,b1.] by A3,Def1;
not x in [.a2,b2.[ by A3,Def4;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1; hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1; hence thesis by A2;
suppose b1 <=' a1;
then A6: [.a1,b1.] c= {a1} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
A8:x in [.a2,b2.[ by A7,Def4;
not x in [.a1,b1.] by A1,A6,A7,TARSKI:def 1;
hence thesis by A8;
end;
hence thesis;
end;
theorem Th37:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] & x in [.a2,b2.[))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in [.a2,b2.[ by A3,Def4;
not x in [.a1,b1.] by A3,Def1;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2;
hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2; hence thesis by A2;
suppose
A6: b2 <=' a2;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in [.a1,b1.] & not x in [.a2,b2.[ by A6,A7,Def1,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th38:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in [.a1,b1.[ by A3,Def4;
not x in [.a2,b2.] by A3,Def1;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1;
hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1;
hence thesis by A2;
suppose b1 <=' a1;
then A6: [.a1,b1.[ = {} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
x in [.a2,b2.] by A7,Def1;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th39:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.]) or (not x in [.a1,b1.[ & x in [.a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a2 <' b2;
then consider x being R_eal such that
A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A3:x in [.a2,b2.] by A2,Def1;
not x in [.a1,b1.[ by A2,Def4;
hence thesis by A3;
suppose that
A4: a1 <' b1 and
A5: b2 <=' a2;
A6: [.a2,b2.] c= {b2} by A5,Th15;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A4,Th17;
A8:x in [.a1,b1.[ by A7,Def4;
not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
hence thesis by A8;
end;
theorem Th40:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.]) or (not x in [.a1,b1.] & x in ].a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a1 <' b1;
then consider x being R_eal such that
A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A3:x in [.a1,b1.] by A2,Def1;
not x in ].a2,b2.] by A2,Def3;
hence thesis by A3;
suppose that
A4: a2 <' b2 and
A5: b1 <=' a1;
A6: [.a1,b1.] c= {a1} by A5,Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
A8:x in ].a2,b2.] by A7,Def3;
not x in [.a1,b1.] by A1,A6,A7,TARSKI:def 1;
hence thesis by A8;
end;
theorem Th41:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.]) or (not x in [.a1,b1.] & x in ].a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a2 <' b2;
then consider x being R_eal such that
A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A3:x in ].a2,b2.] by A2,Def3;
not x in [.a1,b1.] by A2,Def1;
hence thesis by A3;
suppose that
A4:a1 <' b1 and
A5: b2 <=' a2;
consider x being R_eal such that
A6:a1 <' x & x <' b1 & x in REAL by A4,Th17;
x in [.a1,b1.] & not x in ].a2,b2.] by A5,A6,Def1,Th15;
hence thesis;
end;
theorem Th42:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.]) or (not x in ].a1,b1.] & x in [.a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a1 <' b1;
then consider x being R_eal such that
A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A3:x in ].a1,b1.] by A2,Def3;
not x in [.a2,b2.] by A2,Def1;
hence thesis by A3;
suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
A6: ].a1,b1.] = {} by A5,Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
x in [.a2,b2.] by A7,Def1;
hence thesis by A6;
end;
theorem Th43:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.]) or (not x in ].a1,b1.] & x in [.a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a2 <' b2;
then consider x being R_eal such that
A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A3:x in [.a2,b2.] by A2,Def1;
not x in ].a1,b1.] by A2,Def3;
hence thesis by A3;
suppose that
A4: a1 <' b1 and
A5: b2 <=' a2;
A6: [.a2,b2.] c= {b2} by A5,Th15;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A4,Th17;
A8:x in ].a1,b1.] by A7,Def3;
not x in [.a2,b2.] by A1,A6,A7,TARSKI:def 1;
hence thesis by A8;
end;
theorem Th44:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.[) or (not x in [.a1,b1.[ & x in [.a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a1 <' b1;
then consider x being R_eal such that
A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A3:x in [.a1,b1.[ by A2,Def4;
not x in [.a2,b2.[ by A2,Def4;
hence thesis by A3;
suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
A6:[.a1,b1.[ = {} by A5,Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
x in [.a2,b2.[ by A7,Def4;
hence thesis by A6;
end;
theorem Th45:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.[) or (not x in [.a1,b1.[ & x in [.a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a2 <' b2;
then consider x being R_eal such that
A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A3:x in [.a2,b2.[ by A2,Def4;
not x in [.a1,b1.[ by A2,Def4;
hence thesis by A3;
suppose that
A4:a1 <' b1 and
A5: b2 <=' a2;
consider x being R_eal such that
A6:a1 <' x & x <' b1 & x in REAL by A4,Th17;
x in [.a1,b1.[ & not x in [.a2,b2.[ by A5,A6,Def4,Th15;
hence thesis;
end;
theorem Th46:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.]) or (not x in [.a1,b1.[ & x in ].a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a1 <' b1;
then consider x being R_eal such that
A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A3:x in [.a1,b1.[ by A2,Def4;
not x in ].a2,b2.] by A2,Def3;
hence thesis by A3;
suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
A6: [.a1,b1.[ = {} by A5,Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
x in ].a2,b2.] by A7,Def3;
hence thesis by A6;
end;
theorem Th47:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.]) or (not x in [.a1,b1.[ & x in ].a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a2 <' b2;
then consider x being R_eal such that
A2:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A3:x in ].a2,b2.] by A2,Def3;
not x in [.a1,b1.[ by A2,Def4;
hence thesis by A3;
suppose that
A4:a1 <' b1 and
A5: b2 <=' a2;
consider x being R_eal such that
A6:a1 <' x & x <' b1 & x in REAL by A4,Th17;
x in [.a1,b1.[ & not x in ].a2,b2.] by A5,A6,Def4,Th15;
hence thesis;
end;
theorem Th48:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
per cases by A1;
suppose a1 <' b1;
then consider x being R_eal such that
A2:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A3:x in ].a1,b1.] by A2,Def3;
not x in [.a2,b2.[ by A2,Def4;
hence thesis by A3;
suppose that
A4:a2 <' b2 and
A5: b1 <=' a1;
A6: ].a1,b1.] = {} by A5,Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A4,Th17;
x in [.a2,b2.[ by A7,Def4;
hence thesis by A6;
end;
theorem Th49:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.] &
not x in [.a2,b2.[) or (not x in ].a1,b1.] & x in [.a2,b2.[))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in [.a2,b2.[ by A3,Def4;
not x in ].a1,b1.] by A3,Def3;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2; hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2; hence thesis by A2;
suppose
A6: b2 <=' a2;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in ].a1,b1.] & not x in [.a2,b2.[ by A6,A7,Def3,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th50:
a1 <' a2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
proof
assume
A1:a1 <' a2 & (a1 <' b1 or a2 <' b2);
A2:a1 <' b1 implies ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
proof
assume a1 <' b1;
then consider x being R_eal such that
A3:a1 <' x & x <' b1 & x <' a2 & x in REAL by A1,Th18;
A4:x in ].a1,b1.] by A3,Def3;
not x in ].a2,b2.] by A3,Def3;
hence thesis by A4;
end;
per cases by A1;
suppose a1 <' b1;
hence thesis by A2;
suppose
A5:a2 <' b2;
now per cases;
suppose a1 <' b1;
hence thesis by A2;
suppose b1 <=' a1;
then A6: ].a1,b1.] = {} by Th15;
consider x being R_eal such that
A7:a2 <' x & x <' b2 & x in REAL by A5,Th17;
x in ].a2,b2.] by A7,Def3;
hence thesis by A6;
end;
hence thesis;
end;
theorem Th51:
b1 <' b2 & (a1 <' b1 or a2 <' b2) implies
ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
proof
assume
A1:b1 <' b2 & (a1 <' b1 or a2 <' b2);
A2:a2 <' b2 implies ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] & x in ].a2,b2.]))
proof
assume a2 <' b2;
then consider x being R_eal such that
A3:b1 <' x & a2 <' x & x <' b2 & x in REAL by A1,Th19;
A4:x in ].a2,b2.] by A3,Def3;
not x in ].a1,b1.] by A3,Def3;
hence thesis by A4;
end;
per cases by A1;
suppose a2 <' b2;
hence thesis by A2;
suppose
A5:a1 <' b1;
now per cases;
suppose a2 <' b2;
hence thesis by A2;
suppose
A6: b2 <=' a2;
consider x being R_eal such that
A7:a1 <' x & x <' b1 & x in REAL by A5,Th17;
x in ].a1,b1.] & not x in ].a2,b2.] by A6,A7,Def3,Th15;
hence thesis;
end;
hence thesis;
end;
theorem Th52:
(a1 <' b1 &
((A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.]) &
(A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.])))
implies (a1 = a2 & b1 = b2)
proof assume that
A1: a1 <' b1 and
A2: A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.] and
A3: A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.];
per cases;
suppose
A4: A = ].a1,b1.[ & A = ].a2,b2.[;
thus a1 = a2 & b1 = b2
proof
assume
A5:a1 <> a2 or b1 <> b2;
per cases by A5;
suppose
A6: a1 <> a2;
now per cases by A6,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.[) or (not x in ].a1,b1.[ &
x in ].a2,b2.[)) by A1,Th20;
hence thesis by A4;
suppose a2 <' a1;
then ex x being R_eal st ((x in ].a2,b2.[ &
not x in ].a1,b1.[) or (not x in ].a2,b2.[ &
x in ].a1,b1.[)) by A1,Th20;
hence thesis by A4;
end;
hence thesis;
suppose A7: b1 <> b2;
now per cases by A7,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st (x in ].a1,b1.[ &
not x in ].a2,b2.[) or (not x in ].a1,b1.[ &
x in ].a2,b2.[) by A1,Th21;
hence thesis by A4;
suppose b2 <' b1;
then ex x being R_eal st (x in ].a2,b2.[ &
not x in ].a1,b1.[) or (not x in ].a2,b2.[ &
x in ].a1,b1.[) by A1,Th21;
hence thesis by A4;
end;
hence thesis;
end;
suppose
A8: A <> ].a1,b1.[ or A <> ].a2,b2.[;
A9: for a1,a2,b1,b2 holds
(((a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.[) implies
a1 = a2 & b1 = b2)
proof let a1,a2,b1,b2;
assume that
A10:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.[ and
A11:a1 <> a2 or b1 <> b2;
per cases by A11;
suppose
A12: a1 <> a2;
now per cases by A12,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st (x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] &
x in ].a2,b2.[) by A10,Th22;
hence thesis by A10;
suppose a2 <' a1;
then ex x being R_eal st (x in ].a2,b2.[ &
not x in [.a1,b1.]) or (not x in ].a2,b2.[ &
x in [.a1,b1.]) by A10,Th24;
hence thesis by A10;
end;
hence thesis;
suppose A13: b1 <> b2;
now per cases by A13,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st (x in [.a1,b1.] &
not x in ].a2,b2.[) or (not x in [.a1,b1.] &
x in ].a2,b2.[) by A10,Th23;
hence thesis by A10;
suppose b2 <' b1;
then ex x being R_eal st (x in ].a2,b2.[ &
not x in [.a1,b1.]) or (not x in ].a2,b2.[ &
x in [.a1,b1.]) by A10,Th25;
hence thesis by A10;
end;
hence thesis;
end;
A14: for a1,a2,b1,b2 holds
(((a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = [.a2,b2.[) implies
a1 = a2 & b1 = b2)
proof let a1,a2,b1,b2;
assume that
A15:(a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = [.a2,b2.[ and
A16:a1 <> a2 or b1 <> b2;
per cases by A16;
suppose
A17: a1 <> a2;
now per cases by A17,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ &
x in [.a2,b2.[)) by A15,Th26;
hence thesis by A15;
suppose a2 <' a1;
then ex x being R_eal st ((x in [.a2,b2.[ &
not x in ].a1,b1.[) or (not x in [.a2,b2.[ &
x in ].a1,b1.[)) by A15,Th28;
hence thesis by A15;
end;
hence thesis;
suppose A18: b1 <> b2;
now per cases by A18,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st ((x in ].a1,b1.[ &
not x in [.a2,b2.[) or (not x in ].a1,b1.[ &
x in [.a2,b2.[)) by A15,Th27;
hence thesis by A15;
suppose b2 <' b1;
then ex x being R_eal st ((x in [.a2,b2.[ &
not x in ].a1,b1.[) or (not x in [.a2,b2.[ &
x in ].a1,b1.[)) by A15,Th29;
hence thesis by A15;
end;
hence thesis;
end;
A19:
for a1,a2,b1,b2 holds
((a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = ].a2,b2.]) implies
a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
assume
A20:(a1 <' b1 or a2 <' b2) & A = ].a1,b1.[ & A = ].a2,b2.];
assume
A21:a1 <> a2 or b1 <> b2;
per cases by A21;
suppose
A22: a1 <> a2;
now per cases by A22,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in ].a1,b1.[ &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ &
x in ].a2,b2.])) by A20,Th30;
hence thesis by A20;
suppose a2 <' a1;
then ex x being R_eal st ((x in ].a2,b2.] &
not x in ].a1,b1.[) or (not x in ].a2,b2.] &
x in ].a1,b1.[)) by A20,Th32;
hence thesis by A20;
end;
hence thesis;
suppose A23: b1 <> b2;
now per cases by A23,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st (((x in ].a1,b1.[) &
not x in ].a2,b2.]) or (not x in ].a1,b1.[ &
x in ].a2,b2.])) by A20,Th31;
hence thesis by A20;
suppose b2 <' b1;
then ex x being R_eal st ((x in ].a2,b2.] &
not x in ].a1,b1.[) or (not x in ].a2,b2.] &
x in ].a1,b1.[)) by A20,Th33;
hence thesis by A20;
end;
hence thesis;
end;
A24:
(A = [.a1,b1.] & A = [.a2,b2.]) implies
a1 = a2 & b1 = b2
proof
assume
A25: A = [.a1,b1.] & A = [.a2,b2.];
assume
A26:a1 <> a2 or b1 <> b2;
per cases by A26;
suppose
A27: a1 <> a2;
now per cases by A27,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] &
x in [.a2,b2.])) by A1,Th34;
hence thesis by A25;
suppose a2 <' a1;
then ex x being R_eal st ((x in [.a2,b2.] &
not x in [.a1,b1.]) or (not x in [.a2,b2.] &
x in [.a1,b1.])) by A1,Th34;
hence thesis by A25;
end;
hence thesis;
suppose A28: b1 <> b2;
now per cases by A28,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.]) or (not x in [.a1,b1.] &
x in [.a2,b2.])) by A1,Th35;
hence thesis by A25;
suppose b2 <' b1;
then ex x being R_eal st ((x in [.a2,b2.] &
not x in [.a1,b1.]) or (not x in [.a2,b2.] &
x in [.a1,b1.])) by A1,Th35;
hence thesis by A25;
end;
hence thesis;
end;
A29: for a1,a2,b1,b2 holds
((a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = [.a2,b2.[) implies
a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
assume
A30:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = [.a2,b2.[;
assume
A31:a1 <> a2 or b1 <> b2;
per cases by A31;
suppose
A32: a1 <> a2;
now per cases by A32,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] &
x in [.a2,b2.[)) by A30,Th36;
hence thesis by A30;
suppose a2 <' a1;
then ex x being R_eal st ((x in [.a2,b2.[ &
not x in [.a1,b1.]) or (not x in [.a2,b2.[ &
x in [.a1,b1.])) by A30,Th38;
hence thesis by A30;
end;
hence thesis;
suppose A33: b1 <> b2;
now per cases by A33,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st ((x in [.a1,b1.] &
not x in [.a2,b2.[) or (not x in [.a1,b1.] &
x in [.a2,b2.[)) by A30,Th37;
hence thesis by A30;
suppose b2 <' b1;
then ex x being R_eal st ((x in [.a2,b2.[ &
not x in [.a1,b1.]) or (not x in [.a2,b2.[ &
x in [.a1,b1.])) by A30,Th39;
hence thesis by A30;
end;
hence thesis;
end;
A34: for a1,a2,b1,b2 holds
((a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.]) implies
a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
assume
A35:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.] & A = ].a2,b2.];
assume
A36:a1 <> a2 or b1 <> b2;
per cases by A36;
suppose
A37: a1 <> a2;
now per cases by A37,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.]) or (not x in [.a1,b1.] &
x in ].a2,b2.])) by A35,Th40;
hence thesis by A35;
suppose a2 <' a1;
then ex x being R_eal st ((x in ].a2,b2.] &
not x in [.a1,b1.]) or (not x in ].a2,b2.] &
x in [.a1,b1.])) by A35,Th42;
hence thesis by A35;
end;
hence thesis;
suppose A38: b1 <> b2;
now per cases by A38,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st ((x in [.a1,b1.] &
not x in ].a2,b2.]) or (not x in [.a1,b1.] &
x in ].a2,b2.])) by A35,Th41;
hence thesis by A35;
suppose b2 <' b1;
then ex x being R_eal st ((x in ].a2,b2.] &
not x in [.a1,b1.]) or (not x in ].a2,b2.] &
x in [.a1,b1.])) by A35,Th43;
hence thesis by A35;
end;
hence thesis;
end;
A39:
(A = [.a1,b1.[ & A = [.a2,b2.[) implies a1 = a2 & b1 = b2
proof
assume
A40: A = [.a1,b1.[ & A = [.a2,b2.[;
assume
A41:a1 <> a2 or b1 <> b2;
per cases by A41;
suppose
A42: a1 <> a2;
now per cases by A42,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.[) or (not x in [.a1,b1.[ &
x in [.a2,b2.[)) by A1,Th44;
hence thesis by A40;
suppose a2 <' a1;
then ex x being R_eal st ((x in [.a2,b2.[ &
not x in [.a1,b1.[) or (not x in [.a2,b2.[ &
x in [.a1,b1.[)) by A1,Th44;
hence thesis by A40;
end;
hence thesis;
suppose A43: b1 <> b2;
now per cases by A43,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st ((x in [.a1,b1.[ &
not x in [.a2,b2.[) or (not x in [.a1,b1.[ &
x in [.a2,b2.[)) by A1,Th45;
hence thesis by A40;
suppose b2 <' b1;
then ex x being R_eal st ((x in [.a2,b2.[ &
not x in [.a1,b1.[) or (not x in [.a2,b2.[ &
x in [.a1,b1.[)) by A1,Th45;
hence thesis by A40;
end;
hence thesis;
end;
A44: for a1,a2,b1,b2 holds
((a1 <' b1 or a2 <' b2) & A = [.a1,b1.[ & A = ].a2,b2.]) implies
a1 = a2 & b1 = b2
proof let a1,a2,b1,b2;
assume
A45:(a1 <' b1 or a2 <' b2) & A = [.a1,b1.[ & A = ].a2,b2.];
assume
A46:a1 <> a2 or b1 <> b2;
per cases by A46;
suppose
A47: a1 <> a2;
now per cases by A47,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.]) or (not x in [.a1,b1.[ &
x in ].a2,b2.])) by A45,Th46;
hence thesis by A45;
suppose a2 <' a1;
then ex x being R_eal st ((x in ].a2,b2.] &
not x in [.a1,b1.[) or (not x in ].a2,b2.] &
x in [.a1,b1.[)) by A45,Th48;
hence thesis by A45;
end;
hence thesis;
suppose A48: b1 <> b2;
now per cases by A48,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st ((x in [.a1,b1.[ &
not x in ].a2,b2.]) or (not x in [.a1,b1.[ &
x in ].a2,b2.])) by A45,Th47;
hence thesis by A45;
suppose b2 <' b1;
then ex x being R_eal st ((x in ].a2,b2.] &
not x in [.a1,b1.[) or (not x in ].a2,b2.] &
x in [.a1,b1.[)) by A45,Th49;
hence thesis by A45;
end;
hence thesis;
end;
(A = ].a1,b1.] & A = ].a2,b2.]) implies a1 = a2 & b1 = b2
proof
assume
A49: A = ].a1,b1.] & A = ].a2,b2.];
assume
A50:a1 <> a2 or b1 <> b2;
per cases by A50;
suppose
A51: a1 <> a2;
now per cases by A51,SUPINF_1:22;
suppose a1 <' a2;
then ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] &
x in ].a2,b2.])) by A1,Th50;
hence thesis by A49;
suppose a2 <' a1;
then ex x being R_eal st ((x in ].a2,b2.] &
not x in ].a1,b1.]) or (not x in ].a2,b2.] &
x in ].a1,b1.])) by A1,Th50;
hence thesis by A49;
end;
hence thesis;
suppose A52: b1 <> b2;
now per cases by A52,SUPINF_1:22;
suppose b1 <' b2;
then ex x being R_eal st ((x in ].a1,b1.] &
not x in ].a2,b2.]) or (not x in ].a1,b1.] &
x in ].a2,b2.])) by A1,Th51;
hence thesis by A49;
suppose b2 <' b1;
then ex x being R_eal st ((x in ].a2,b2.] & not x in ].a1,b1.]) or
(not x in ].a2,b2.] & x in ].a1,b1.])) by A1,Th51;
hence thesis by A49;
end;
hence thesis;
end;
hence thesis by A1,A2,A3,A8,A9,A14,A19,A24,A29,A34,A39,A44;
end;
definition let A be Interval;
func vol A -> R_eal means
:Def10:ex a,b being R_eal st
((A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]) &
(a <' b implies it = b - a) &
(b <=' a implies it = 0.));
existence
proof
A is open_interval or A is closed_interval or
A is right_open_interval or A is left_open_interval by Def9;
then (ex a,b being R_eal st (a <=' b & A = ].a,b.[)) or
(ex a,b being R_eal st (a <=' b & A = [.a,b.])) or
(ex a,b being R_eal st (a <=' b & A = [.a,b.[)) or
(ex a,b being R_eal st (a <=' b & A = ].a,b.]))
by Def5,Def6,Def7,Def8;
then consider a,b being R_eal such that
A1:A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.];
b <=' a implies ex x being R_eal st
((a <' b implies x = b - a) & (b <=' a implies x = 0.));
then ex x being R_eal st
((a <' b implies x = b - a) & (b <=' a implies x = 0.));
hence thesis by A1;
end;
uniqueness
proof
let x1,x2 be R_eal;
given a1,b1 being R_eal such that
A2: ((A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.]) &
(a1 <' b1 implies x1 = b1 - a1) &
(b1 <=' a1 implies x1 = 0.));
given a2,b2 being R_eal such that
A3: ((A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.]) &
(a2 <' b2 implies x2 = b2 - a2) &
(b2 <=' a2 implies x2 = 0.));
per cases;
suppose
a1 <' b1 & a2 <' b2;
then a1 = a2 & b1 = b2 by A2,A3,Th52;
hence thesis by A2,A3;
suppose
A4:a1 <' b1 & b2 <=' a2;
then a1 = a2 & b1 = b2 by A2,A3,Th52;
hence thesis by A4;
suppose
A5:b1 <=' a1 & a2 <' b2;
then a1 = a2 & b1 = b2 by A2,A3,Th52;
hence thesis by A5;
suppose b1 <=' a1 & b2 <=' a2;hence thesis by A2,A3;
end;
end;
theorem
for A being open_interval Subset of REAL holds
for a,b being R_eal holds
A = ].a,b.[ implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.)) by Def10;
theorem
for A being closed_interval Subset of REAL holds
for a,b being R_eal holds
A = [.a,b.] implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.)) by Def10;
theorem
for A being right_open_interval Subset of REAL holds
for a,b being R_eal holds
A = [.a,b.[ implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.)) by Def10;
theorem
for A being left_open_interval Subset of REAL holds
for a,b being R_eal holds
A = ].a,b.] implies
((a <' b implies vol(A) = b - a) &
(b <=' a implies vol(A) = 0.)) by Def10;
theorem
for a,b,c being R_eal holds
(a = -infty & b in REAL & c = +infty &
(A = ].a,b.[ or A = ].b,c.[ or A = [.a,b.] or A = [.b,c.] or
A = [.a,b.[ or A = [.b,c.[ or A = ].a,b.] or A = ].b,c.]))
implies vol(A) = +infty
proof
let a,b,c be R_eal;
assume
A1:a = -infty & b in REAL & c = +infty &
(A = ].a,b.[ or A = ].b,c.[ or A = [.a,b.] or A = [.b,c.] or
A = [.a,b.[ or A = [.b,c.[ or A = ].a,b.] or A = ].b,c.]);
per cases by A1;
suppose A = ].a,b.[;
then A = ].a,b.[ & a <' b by A1,SUPINF_1:31;
then vol(A) = b - a by Def10;
hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
suppose A = ].b,c.[;
then A = ].b,c.[ & b <' c by A1,SUPINF_1:31;
then A2:vol(A) = c - b by Def10;
not ((c = +infty & b = +infty) or (c = -infty & b = -infty
)) by A1,SUPINF_1:def 1;
hence thesis by A1,A2,SUPINF_2:6;
suppose A3:A = [.a,b.];
a <' b by A1,SUPINF_1:31;
then vol(A) = b - a by A3,Def10;
hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
suppose A4:A = [.b,c.];
b <' c by A1,SUPINF_1:31;
then A5:vol(A) = c - b by A4,Def10;
not ((c = +infty & b = +infty) or (c = -infty & b = -infty
)) by A1,SUPINF_1:def 1;
hence thesis by A1,A5,SUPINF_2:6;
suppose A6:A = [.a,b.[;
a <' b by A1,SUPINF_1:31;
then vol(A) = b - a by A6,Def10;
hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
suppose A = [.b,c.[;
then A = [.b,c.[ & b <' c by A1,SUPINF_1:31;
then A7:vol(A) = c - b by Def10;
not ((c = +infty & b = +infty) or (c = -infty & b = -infty))
by A1,SUPINF_1:def 1;
hence thesis by A1,A7,SUPINF_2:6;
suppose A = ].a,b.];
then A = ].a,b.] & a <' b by A1,SUPINF_1:31;
then vol(A) = b - a by Def10;
hence thesis by A1,SUPINF_1:6,SUPINF_2:7;
suppose A = ].b,c.];
then A = ].b,c.] & b <' c by A1,SUPINF_1:31;
then A8:vol(A) = c - b by Def10;
not ((c = +infty & b = +infty) or (c = -infty & b = -infty))
by A1,SUPINF_1:def 1;
hence thesis by A1,A8,SUPINF_2:6;
end;
theorem
for a,b being R_eal holds
(a = -infty & b = +infty &
(A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]))
implies vol(A) = +infty
proof
let a,b be R_eal;
assume
A1:a = -infty & b = +infty &
(A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.]);
then a <' b by SUPINF_1:29,SUPINF_2:19;
then vol(A) = b - a by A1,Def10
.= +infty by A1,SUPINF_1:14,SUPINF_2:6;
hence thesis;
end;
definition
cluster empty Interval;
existence
proof
{} is open_interval Subset of REAL
proof
ex a,b being R_eal st a <=' b & {} = ].a,b.[
proof
consider c being R_eal;
consider a,b being R_eal such that
A1:a = c & b = c;
take a,b;
thus thesis by A1,Th13;
end;
hence thesis by Def5;
end;
hence thesis;
end;
end;
definition
redefine func {} -> empty Interval;
coherence
proof
{} is open_interval Subset of REAL
proof
ex a,b being R_eal st (a <=' b & {} = ].a,b.[)
proof
consider c being R_eal;
consider a,b being R_eal such that
A1:a = c & b = c;
take a,b;
thus thesis by A1,Th13;
end;
hence thesis by Def5;
end;
hence thesis;
end;
end;
canceled;
theorem Th60:
vol {} = 0.
proof
{} = ].0.,0..[ by Th13;
hence thesis by Def10;
end;
theorem Th61:
(A c= B & B =[.a,b.] & b <=' a) implies
(vol(A) = 0. & vol(B) = 0.)
proof
assume
A1:A c= B & B =[.a,b.] & b <=' a;
A is open_interval or A is closed_interval or
A is right_open_interval or A is left_open_interval by Def9;
then (ex c,d being R_eal st (c <=' d & A = ].c,d.[)) or
(ex c,d being R_eal st (c <=' d & A = [.c,d.])) or
(ex c,d being R_eal st (c <=' d & A = [.c,d.[)) or
(ex c,d being R_eal st (c <=' d & A = ].c,d.]))
by Def5,Def6,Def7,Def8;
then consider c,d being R_eal such that
A2:c <=' d &
(A = ].c,d.[ or A = [.c,d.] or A = [.c,d.[ or A = ].c,d.]);
c <' d implies vol(A) = 0.
proof
assume
A3:c <' d;
B c= {a} by A1,Th15;
then A4:A c= {a} by A1,XBOOLE_1:1;
per cases by A2;
suppose
A5:A = ].c,d.[;
A = {}
proof
assume
A6: A <> {};
consider x being Element of A;
A c= ExtREAL by XBOOLE_1:1;
then reconsider x as R_eal by A6,TARSKI:def 3;
A7:c <' x & x <' d & x in REAL by A5,A6,Def2;
x in {a} by A4,A6,TARSKI:def 3;
then A8:x = a by TARSKI:def 1;
consider y being R_eal such that
A9:c <' y & y <' x & y in REAL by A7,Th17;
y <' d by A7,A9,SUPINF_1:29;
then y in A by A5,A9,Def2; hence thesis by A4,A8,A9,TARSKI:def 1
;
end;
hence thesis by Th60;
suppose
A10:A = [.c,d.];
consider x being R_eal such that
A11:c <' x & x <' d & x in REAL by A3,Th17;
x in A by A10,A11,Def1;
then A12:x = a by A4,TARSKI:def 1;
consider y being R_eal such that
A13:c <' y & y <' x & y in REAL by A11,Th17;
c <=' y & y <=' d & y in REAL by A11,A13,SUPINF_1:29;
then y in A by A10,Def1; hence thesis by A4,A12,A13,TARSKI:def 1;
suppose
A14:A = [.c,d.[;
A = {}
proof
assume
A15: A <> {};
consider x being Element of A;
A c= ExtREAL by XBOOLE_1:1;
then reconsider x as R_eal by A15,TARSKI:def 3;
A16:c <=' x & x <' d & x in REAL by A14,A15,Def4;
x in {a} by A4,A15,TARSKI:def 3;
then A17:x = a by TARSKI:def 1;
consider y being R_eal such that
A18:x <' y & y <' d & y in REAL by A16,Th17;
c <=' y by A16,A18,SUPINF_1:29;
then y in A by A14,A18,Def4; hence thesis by A4,A17,A18,TARSKI:
def 1;
end;
hence thesis by Th60;
suppose
A19:A = ].c,d.];
A = {}
proof
assume
A20: A <> {};
consider x being Element of A;
A c= ExtREAL by XBOOLE_1:1;
then reconsider x as R_eal by A20,TARSKI:def 3;
A21:c <' x & x <=' d & x in REAL by A19,A20,Def3;
x in {a} by A4,A20,TARSKI:def 3;
then A22:x = a by TARSKI:def 1;
consider y being R_eal such that
A23:c <' y & y <' x & y in REAL by A21,Th17;
y <=' d by A21,A23,SUPINF_1:29;
then y in A by A19,A23,Def3; hence thesis by A4,A22,A23,TARSKI:
def 1;
end;
hence thesis by Th60;
end;
hence thesis by A1,A2,Def10;
end;
theorem Th62:
A c= B implies vol A <=' vol B
proof
assume
A1:A c= B;
A is open_interval or A is closed_interval or
A is right_open_interval or A is left_open_interval by Def9;
then (ex a1,b1 being R_eal st (a1 <=' b1 & A =].a1,b1.[)) or
(ex a1,b1 being R_eal st (a1 <=' b1 & A =[.a1,b1.])) or
(ex a1,b1 being R_eal st (a1 <=' b1 & A =[.a1,b1.[)) or
(ex a1,b1 being R_eal st (a1 <=' b1 & A =].a1,b1.]))
by Def5,Def6,Def7,Def8;
then consider a1,b1 being R_eal such that
A2:A =].a1,b1.[ or A =[.a1,b1.] or A =[.a1,b1.[ or A =].a1,b1.];
B is open_interval or B is closed_interval or
B is right_open_interval or B is left_open_interval by Def9;
then (ex a2,b2 being R_eal st (a2 <=' b2 & B =].a2,b2.[)) or
(ex a2,b2 being R_eal st (a2 <=' b2 & B =[.a2,b2.])) or
(ex a2,b2 being R_eal st (a2 <=' b2 & B =[.a2,b2.[)) or
(ex a2,b2 being R_eal st (a2 <=' b2 & B =].a2,b2.]))
by Def5,Def6,Def7,Def8;
then consider a2,b2 being R_eal such that
A3:B =].a2,b2.[ or B =[.a2,b2.] or B =[.a2,b2.[ or B =].a2,b2.];
per cases by A2,A3;
suppose
A4: A = ].a1,b1.[ & B = ].a2,b2.[;
thus vol(A) <=' vol(B)
proof
per cases;
suppose
A5:a1 <' b1 & a2 <' b2;
A6:b1 <=' b2 & a2 <=' a1
proof
assume
A7: not b1 <=' b2 or not a2 <=' a1;
per cases by A7;
suppose b2 <' b1;
then consider x being R_eal such that
A8:a1 <' x & b2 <' x & x <' b1 & x in REAL by A5,Th19;
x in ].a1,b1.[ & not x <=' b2 by A8,Def2;
hence thesis by A1,A4,Def2;
suppose a1 <' a2;
then consider x being R_eal such that
A9:a1 <' x & x <' a2 & x <' b1 & x in REAL by A5,Th18;
x in ].a1,b1.[ & not a2 <=' x by A9,Def2;
hence thesis by A1,A4,Def2;
end;
A10: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A5;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A4,A5,Def10;
hence thesis by A6,A10,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A4,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A11:b1 <=' a1 & a2 <' b2;
then A12:vol(A) = 0. by A4,Def10;
A13:vol(B) = b2 - a2 by A4,A11,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty
) & a2 <=' b2 by A11;
hence thesis by A12,A13,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A4,Def10;
hence thesis;
end;
suppose
A14: A = ].a1,b1.[ & B = [.a2,b2.];
thus vol A <=' vol B
proof
per cases;
suppose
A15:a1 <' b1 & a2 <' b2;
A16:b1 <=' b2 & a2 <=' a1
proof
assume
A17: not b1 <=' b2 or not a2 <=' a1;
per cases by A17;
suppose b2 <' b1;
then consider x being R_eal such that
A18:a1 <' x & b2 <' x & x <' b1 & x in REAL by A15,Th19;
x in ].a1,b1.[ & not x <=' b2 by A18,Def2;
hence thesis by A1,A14,Def1;
suppose a1 <' a2;
then consider x being R_eal such that
A19:a1 <' x & x <' a2 & x <' b1 & x in REAL by A15,Th18;
x in ].a1,b1.[ & not a2 <=' x by A19,Def2;
hence thesis by A1,A14,Def1;
end;
A20: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A15;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A14,A15,Def10;
hence thesis by A16,A20,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A1,A14,Th61;
hence thesis;
suppose
A21:b1 <=' a1 & a2 <' b2;
then A22:vol(A) = 0. by A14,Def10;
A23:vol(B) = b2 - a2 by A14,A21,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A21;
hence thesis by A22,A23,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A14,Def10;
hence thesis;
end;
suppose
A24: A = ].a1,b1.[ & B = [.a2,b2.[;
thus vol(A) <=' vol(B)
proof
per cases;
suppose
A25:a1 <' b1 & a2 <' b2;
A26:b1 <=' b2 & a2 <=' a1
proof
assume
A27: not b1 <=' b2 or not a2 <=' a1;
per cases by A27;
suppose b2 <' b1;
then consider x being R_eal such that
A28:a1 <' x & b2 <' x & x <' b1 & x in REAL by A25,Th19;
x in ].a1,b1.[ & not x <=' b2 by A28,Def2;
hence thesis by A1,A24,Def4;
suppose a1 <' a2;
then consider x being R_eal such that
A29:a1 <' x & x <' a2 & x <' b1 & x in REAL by A25,Th18;
x in ].a1,b1.[ & not a2 <=' x by A29,Def2;
hence thesis by A1,A24,Def4;
end;
A30: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A25;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A24,A25,Def10;
hence thesis by A26,A30,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A24,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A31:b1 <=' a1 & a2 <' b2;
then A32:vol(A) = 0. by A24,Def10;
A33:vol(B) = b2 - a2 by A24,A31,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A31;
hence thesis by A32,A33,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A24,Def10;
hence thesis;
end;
suppose
A34: A = ].a1,b1.[ & B = ].a2,b2.];
thus vol(A) <=' vol(B)
proof
per cases;
suppose
A35:a1 <' b1 & a2 <' b2;
A36:b1 <=' b2 & a2 <=' a1
proof
assume
A37: not b1 <=' b2 or not a2 <=' a1;
per cases by A37;
suppose b2 <' b1;
then consider x being R_eal such that
A38:a1 <' x & b2 <' x & x <' b1 & x in REAL by A35,Th19;
x in ].a1,b1.[ & not x <=' b2 by A38,Def2;
hence thesis by A1,A34,Def3;
suppose a1 <' a2;
then consider x being R_eal such that
A39:a1 <' x & x <' a2 & x <' b1 & x in REAL by A35,Th18;
x in ].a1,b1.[ & not a2 <=' x by A39,Def2;
hence thesis by A1,A34,Def3;
end;
A40: (not (b1 = +infty & a1 = +infty) & not (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A35;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A34,A35,Def10;
hence thesis by A36,A40,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A34,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A41:b1 <=' a1 & a2 <' b2;
then A42:vol(A) = 0. by A34,Def10;
A43:vol(B) = b2 - a2 by A34,A41,Def10;
(b2 <> -infty or a2 <> -infty) & (b2 <> +infty or a2 <> +infty) &
a2 <=' b2 by A41;
hence thesis by A42,A43,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A34,Def10;
hence thesis;
end;
suppose
A44: A = [.a1,b1.] & B = ].a2,b2.[;
thus vol(A) <=' vol(B)
proof
per cases;
suppose
A45:a1 <' b1 & a2 <' b2;
A46:b1 <=' b2 & a2 <=' a1
proof
assume
A47: not b1 <=' b2 or not a2 <=' a1;
per cases by A47;
suppose b2 <' b1;
then consider x being R_eal such that
A48:a1 <' x & b2 <' x & x <' b1 & x in REAL by A45,Th19;
x in [.a1,b1.] & not x <=' b2 by A48,Def1;
hence thesis by A1,A44,Def2;
suppose a1 <' a2;
then consider x being R_eal such that
A49:a1 <' x & x <' a2 & x <' b1 & x in REAL by A45,Th18;
x in [.a1,b1.] & not a2 <=' x by A49,Def1;
hence thesis by A1,A44,Def2;
end;
A50: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A45;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A44,A45,Def10;
hence thesis by A46,A50,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A44,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A51:b1 <=' a1 & a2 <' b2;
then A52:vol A = 0. by A44,Def10;
A53:vol B = b2 - a2 by A44,A51,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A51;
hence thesis by A52,A53,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol A = 0. & vol B = 0. by A44,Def10;
hence thesis;
end;
suppose
A54: A = [.a1,b1.] & B = [.a2,b2.];
thus vol A <=' vol B
proof
per cases;
suppose
A55:a1 <' b1 & a2 <' b2;
A56:b1 <=' b2 & a2 <=' a1
proof
assume
A57: not b1 <=' b2 or not a2 <=' a1;
per cases by A57;
suppose b2 <' b1;
then consider x being R_eal such that
A58:a1 <' x & b2 <' x & x <' b1 & x in REAL by A55,Th19;
x in [.a1,b1.] & not x <=' b2 by A58,Def1;
hence thesis by A1,A54,Def1;
suppose a1 <' a2;
then consider x being R_eal such that
A59:a1 <' x & x <' a2 & x <' b1 & x in REAL by A55,Th18;
x in [.a1,b1.] & not a2 <=' x by A59,Def1;
hence thesis by A1,A54,Def1;
end;
A60: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A55;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A54,A55,Def10;
hence thesis by A56,A60,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then vol A = 0. & vol B = 0. by A1,A54,Th61;
hence thesis;
suppose
A61:b1 <=' a1 & a2 <' b2;
then A62:vol A = 0. by A54,Def10;
A63:vol B = b2 - a2 by A54,A61,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A61;
hence thesis by A62,A63,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol A = 0. & vol B = 0. by A54,Def10;
hence thesis;
end;
suppose
A64: A = [.a1,b1.] & B = [.a2,b2.[;
thus vol A <=' vol B
proof
per cases;
suppose
A65:a1 <' b1 & a2 <' b2;
A66:b1 <=' b2 & a2 <=' a1
proof
assume
A67: not b1 <=' b2 or not a2 <=' a1;
per cases by A67;
suppose b2 <' b1;
then consider x being R_eal such that
A68:a1 <' x & b2 <' x & x <' b1 & x in REAL by A65,Th19;
x in [.a1,b1.] & not x <=' b2 by A68,Def1;
hence thesis by A1,A64,Def4;
suppose a1 <' a2;
then consider x being R_eal such that
A69:a1 <' x & x <' a2 & x <' b1 & x in REAL by A65,Th18;
x in [.a1,b1.] & not a2 <=' x by A69,Def1;
hence thesis by A1,A64,Def4;
end;
A70: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A65;
vol A = b1 - a1 & vol(B) = b2 - a2 by A64,A65,Def10;
hence thesis by A66,A70,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A64,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A71:b1 <=' a1 & a2 <' b2;
then A72:vol A = 0. by A64,Def10;
A73:vol B = b2 - a2 by A64,A71,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A71;
hence thesis by A72,A73,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol A = 0. & vol B = 0. by A64,Def10;
hence thesis;
end;
suppose
A74: A = [.a1,b1.] & B = ].a2,b2.];
thus vol A <=' vol B
proof
per cases;
suppose
A75:a1 <' b1 & a2 <' b2;
A76:b1 <=' b2 & a2 <=' a1
proof
assume
A77: not b1 <=' b2 or not a2 <=' a1;
per cases by A77;
suppose b2 <' b1;
then consider x being R_eal such that
A78:a1 <' x & b2 <' x & x <' b1 & x in REAL by A75,Th19;
x in [.a1,b1.] & not x <=' b2 by A78,Def1;
hence thesis by A1,A74,Def3;
suppose a1 <' a2;
then consider x being R_eal such that
A79:a1 <' x & x <' a2 & x <' b1 & x in REAL by A75,Th18;
x in [.a1,b1.] & not a2 <=' x by A79,Def1;
hence thesis by A1,A74,Def3;
end;
A80: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A75;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A74,A75,Def10;
hence thesis by A76,A80,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A74,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A81:b1 <=' a1 & a2 <' b2;
then A82:vol(A) = 0. by A74,Def10;
A83:vol(B) = b2 - a2 by A74,A81,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A81;
hence thesis by A82,A83,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A74,Def10;
hence thesis;
end;
suppose
A84: A = ].a1,b1.] & B = ].a2,b2.[;
thus vol A <=' vol B
proof
per cases;
suppose
A85:a1 <' b1 & a2 <' b2;
A86:b1 <=' b2 & a2 <=' a1
proof
assume
A87: not b1 <=' b2 or not a2 <=' a1;
per cases by A87;
suppose b2 <' b1;
then consider x being R_eal such that
A88:a1 <' x & b2 <' x & x <' b1 & x in REAL by A85,Th19;
x in ].a1,b1.] & not x <=' b2 by A88,Def3;
hence thesis by A1,A84,Def2;
suppose a1 <' a2;
then consider x being R_eal such that
A89:a1 <' x & x <' a2 & x <' b1 & x in REAL by A85,Th18;
x in ].a1,b1.] & not a2 <=' x by A89,Def3;
hence thesis by A1,A84,Def2;
end;
A90: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A85;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A84,A85,Def10;
hence thesis by A86,A90,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A84,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A91:b1 <=' a1 & a2 <' b2;
then A92:vol(A) = 0. by A84,Def10;
A93:vol(B) = b2 - a2 by A84,A91,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A91;
hence thesis by A92,A93,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A84,Def10;
hence thesis;
end;
suppose
A94: A = ].a1,b1.] & B = [.a2,b2.];
thus vol A <=' vol B
proof
per cases;
suppose
A95:a1 <' b1 & a2 <' b2;
A96:b1 <=' b2 & a2 <=' a1
proof
assume
A97: not b1 <=' b2 or not a2 <=' a1;
per cases by A97;
suppose b2 <' b1;
then consider x being R_eal such that
A98:a1 <' x & b2 <' x & x <' b1 & x in REAL by A95,Th19;
x in ].a1,b1.] & not x <=' b2 by A98,Def3;
hence thesis by A1,A94,Def1;
suppose a1 <' a2;
then consider x being R_eal such that
A99:a1 <' x & x <' a2 & x <' b1 & x in REAL by A95,Th18;
x in ].a1,b1.] & not a2 <=' x by A99,Def3; hence thesis by A1,A94,
Def1
;
end;
A100: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A95;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A94,A95,Def10;
hence thesis by A96,A100,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A1,A94,Th61;
hence thesis;
suppose
A101:b1 <=' a1 & a2 <' b2;
then A102:vol(A) = 0. by A94,Def10;
A103:vol(B) = b2 - a2 by A94,A101,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A101;
hence thesis by A102,A103,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A94,Def10;
hence thesis;
end;
suppose
A104: A = ].a1,b1.] & B = [.a2,b2.[;
thus vol A <=' vol B
proof
per cases;
suppose
A105:a1 <' b1 & a2 <' b2;
A106:b1 <=' b2 & a2 <=' a1
proof
assume
A107: not b1 <=' b2 or not a2 <=' a1;
per cases by A107;
suppose b2 <' b1;
then consider x being R_eal such that
A108:a1 <' x & b2 <' x & x <' b1 & x in REAL by A105,Th19;
x in ].a1,b1.] & not x <=' b2 by A108,Def3;
hence thesis by A1,A104,Def4;
suppose a1 <' a2;
then consider x being R_eal such that
A109:a1 <' x & x <' a2 & x <' b1 & x in REAL by A105,Th18;
x in ].a1,b1.] & not a2 <=' x by A109,Def3;
hence thesis by A1,A104,Def4;
end;
A110: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A105;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A104,A105,Def10;
hence thesis by A106,A110,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A104,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A111:b1 <=' a1 & a2 <' b2;
then A112:vol(A) = 0. by A104,Def10;
A113:vol(B) = b2 - a2 by A104,A111,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A111;
hence thesis by A112,A113,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A104,Def10;
hence thesis;
end;
suppose
A114: A = ].a1,b1.] & B = ].a2,b2.];
thus vol A <=' vol B
proof
per cases;
suppose
A115:a1 <' b1 & a2 <' b2;
A116:b1 <=' b2 & a2 <=' a1
proof
assume
A117: not b1 <=' b2 or not a2 <=' a1;
per cases by A117;
suppose b2 <' b1;
then consider x being R_eal such that
A118:a1 <' x & b2 <' x & x <' b1 & x in REAL by A115,Th19;
x in ].a1,b1.] & not x <=' b2 by A118,Def3;
hence thesis by A1,A114,Def3;
suppose a1 <' a2;
then consider x being R_eal such that
A119:a1 <' x & x <' a2 & x <' b1 & x in REAL by A115,Th18;
x in ].a1,b1.] & not a2 <=' x by A119,Def3;
hence thesis by A1,A114,Def3;
end;
A120: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A115;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A114,A115,Def10;
hence thesis by A116,A120,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A114,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A121:b1 <=' a1 & a2 <' b2;
then A122:vol(A) = 0. by A114,Def10;
A123:vol(B) = b2 - a2 by A114,A121,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A121;
hence thesis by A122,A123,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A114,Def10;
hence thesis;
end;
suppose
A124: A = [.a1,b1.[ & B = ].a2,b2.[;
thus vol A <=' vol B
proof
per cases;
suppose
A125:a1 <' b1 & a2 <' b2;
A126:b1 <=' b2 & a2 <=' a1
proof
assume
A127: not b1 <=' b2 or not a2 <=' a1;
per cases by A127;
suppose b2 <' b1;
then consider x being R_eal such that
A128:a1 <' x & b2 <' x & x <' b1 & x in REAL by A125,Th19;
x in [.a1,b1.[ & not x <=' b2 by A128,Def4;
hence thesis by A1,A124,Def2;
suppose a1 <' a2;
then consider x being R_eal such that
A129:a1 <' x & x <' a2 & x <' b1 & x in REAL by A125,Th18;
x in [.a1,b1.[ & not a2 <=' x by A129,Def4;
hence thesis by A1,A124,Def2;
end;
A130: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A125;
vol A = b1 - a1 & vol(B) = b2 - a2 by A124,A125,Def10;
hence thesis by A126,A130,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A124,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A131:b1 <=' a1 & a2 <' b2;
then A132:vol(A) = 0. by A124,Def10;
A133:vol(B) = b2 - a2 by A124,A131,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A131;
hence thesis by A132,A133,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A124,Def10;
hence thesis;
end;
suppose
A134: A = [.a1,b1.[ & B = [.a2,b2.];
thus vol A <=' vol B
proof
per cases;
suppose
A135:a1 <' b1 & a2 <' b2;
A136:b1 <=' b2 & a2 <=' a1
proof
assume
A137: not b1 <=' b2 or not a2 <=' a1;
per cases by A137;
suppose b2 <' b1;
then consider x being R_eal such that
A138:a1 <' x & b2 <' x & x <' b1 & x in REAL by A135,Th19;
x in [.a1,b1.[ & not x <=' b2 by A138,Def4; hence thesis by A1,A134,
Def1
;
suppose a1 <' a2;
then consider x being R_eal such that
A139:a1 <' x & x <' a2 & x <' b1 & x in REAL by A135,Th18;
x in [.a1,b1.[ & not a2 <=' x by A139,Def4; hence thesis by A1,A134,
Def1
;
end;
A140:not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A135;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A134,A135,Def10;
hence thesis by A136,A140,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then vol A = 0. & vol B = 0. by A1,A134,Th61;
hence thesis;
suppose
A141:b1 <=' a1 & a2 <' b2;
then A142:vol(A) = 0. by A134,Def10;
A143:vol(B) = b2 - a2 by A134,A141,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A141;
hence thesis by A142,A143,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A134,Def10;
hence thesis;
end;
suppose
A144: A = [.a1,b1.[ & B = [.a2,b2.[;
thus vol A <=' vol B
proof
per cases;
suppose
A145:a1 <' b1 & a2 <' b2;
A146:b1 <=' b2 & a2 <=' a1
proof
assume
A147: not b1 <=' b2 or not a2 <=' a1;
per cases by A147;
suppose b2 <' b1;
then consider x being R_eal such that
A148:a1 <' x & b2 <' x & x <' b1 & x in REAL by A145,Th19;
x in [.a1,b1.[ & not x <=' b2 by A148,Def4;
hence thesis by A1,A144,Def4;
suppose a1 <' a2;
then consider x being R_eal such that
A149:a1 <' x & x <' a2 & x <' b1 & x in REAL by A145,Th18;
x in [.a1,b1.[ & not a2 <=' x by A149,Def4; hence thesis by A1,A144,
Def4
;
end;
A150:not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A145;
vol A = b1 - a1 & vol B = b2 - a2 by A144,A145,Def10;
hence thesis by A146,A150,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A144,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A151:b1 <=' a1 & a2 <' b2;
then A152:vol(A) = 0. by A144,Def10;
A153:vol(B) = b2 - a2 by A144,A151,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A151;
hence thesis by A152,A153,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A144,Def10;
hence thesis;
end;
suppose
A154: A = [.a1,b1.[ & B = ].a2,b2.];
thus vol(A) <=' vol(B)
proof
per cases;
suppose
A155:a1 <' b1 & a2 <' b2;
A156:b1 <=' b2 & a2 <=' a1
proof
assume
A157: not b1 <=' b2 or not a2 <=' a1;
per cases by A157;
suppose b2 <' b1;
then consider x being R_eal such that
A158:a1 <' x & b2 <' x & x <' b1 & x in REAL by A155,Th19;
x in [.a1,b1.[ & not x <=' b2 by A158,Def4;
hence thesis by A1,A154,Def3;
suppose a1 <' a2;
then consider x being R_eal such that
A159:a1 <' x & x <' a2 & x <' b1 & x in REAL by A155,Th18;
x in [.a1,b1.[ & not a2 <=' x by A159,Def4;
hence thesis by A1,A154,Def3;
end;
A160: not ((b1 = +infty & a1 = +infty) or (b1 = -infty & a1 = -infty)) &
not ((b2 = +infty & a2 = +infty) or (b2 = -infty & a2 = -infty)) by A155;
vol(A) = b1 - a1 & vol(B) = b2 - a2 by A154,A155,Def10;
hence thesis by A156,A160,SUPINF_2:15;
suppose a1 <' b1 & b2 <=' a2;
then B = {} by A154,Th15;
hence thesis by A1,XBOOLE_1:3;
suppose
A161:b1 <=' a1 & a2 <' b2;
then A162:vol(A) = 0. by A154,Def10;
A163:vol(B) = b2 - a2 by A154,A161,Def10;
not (b2 = -infty & a2 = -infty) & not (b2 = +infty & a2 = +infty) &
a2 <=' b2 by A161;
hence thesis by A162,A163,Th2;
suppose b1 <=' a1 & b2 <=' a2;
then vol(A) = 0. & vol(B) = 0. by A154,Def10;
hence thesis;
end;
end;
theorem
0. <=' vol(A)
proof
{} c= A by XBOOLE_1:2;
hence thesis by Th60,Th62;
end;