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;