Copyright (c) 2002 Association of Mizar Users
environ
vocabulary ARYTM, BOOLE, SQUARE_1, RCOMP_1;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
SQUARE_1, RCOMP_1;
constructors SQUARE_1, RCOMP_1, XCMPLX_0, MEMBERED;
clusters XREAL_0, MEMBERED;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
theorems AXIOMS, TARSKI, SUBSET_1, REAL_1, SQUARE_1, XREAL_0, RCOMP_1,
TOPREAL5, JORDAN6, XBOOLE_0, JGRAPH_3;
schemes DOMAIN_1;
begin
reserve s,g,h,r,p,p1,p2,q,q1,q2,x,y,z for real number;
canceled;
theorem Th2:
y < x & z < x iff max(y,z) < x
proof
thus y < x & z < x implies max(y,z) < x by SQUARE_1:49;
y <= max(y,z) & z <= max(y,z) by SQUARE_1:46;
hence thesis by AXIOMS:22;
end;
definition let g,s be real number;
func [. g,s .[ -> Subset of REAL equals :Def1:
{ r where r is Real : g<=r & r<s };
coherence
proof
defpred P[Real] means g<=$1 & $1<s;
{ r where r is Real : P[r] } is Subset of REAL from SubsetD;
hence thesis;
end;
func ]. g,s .] -> Subset of REAL equals :Def2:
{ r where r is Real : g<r & r<=s };
coherence
proof
defpred P[Real] means g<$1 & $1<=s;
{ r where r is Real : P[r] } is Subset of REAL from SubsetD;
hence thesis;
end;
end;
theorem Th3:
r in [.p,q.[ iff p<=r & r<q
proof
thus r in [.p,q.[ implies p<=r & r<q
proof assume r in [.p,q.[;
then r in {s where s is Real: p<=s & s<q} by Def1;
then consider s being Real such that
A1: r=s & p<=s & s<q;
thus thesis by A1;
end;
assume A2: p<=r & r<q;
reconsider s2=r as Real by XREAL_0:def 1;
p<=s2 & s2<q by A2;
then r in {s where s is Real: p<=s & s<q};
hence thesis by Def1;
end;
theorem Th4:
r in ].p,q.] iff p<r & r<=q
proof
thus r in ].p,q.] implies p<r & r<=q
proof assume r in ].p,q.];
then r in {s where s is Real: p<s & s<=q} by Def2;
then consider s being Real such that
A1: r=s & p<s & s<=q;
thus thesis by A1;
end;
assume A2: p<r & r<=q;
reconsider s2=r as Real by XREAL_0:def 1;
p<s2 & s2<=q by A2;
then r in {s where s is Real: p<s & s<=q};
hence thesis by Def2;
end;
:: Note: r in [.p,q.] iff p<=r & r<=q by TOPREAL5:1
:: r in ].p,q.[ iff p<r & r<q by JORDAN6:45
theorem
for g,s st g<s holds [.g,s.[ = ].g,s.[ \/ {g}
proof let g,s such that A1: g<s;
thus [.g,s.[ c= ].g,s.[ \/ {g}
proof let x be set; assume that A2: x in [.g,s.[ and
A3: not x in ].g,s.[ \/ {g};
x in {r where r is Real: g<=r & r<s} by A2,Def1;
then A4: ex r be Real st r=x & g<=r & r<s;
then reconsider x as Real;
A5: not x in ].g,s.[ & not x in {g} by A3,XBOOLE_0:def 2;
then A6: (not x in ].g,s.[) & x<> g by TARSKI:def 1;
not (x in {q where q is Real: g<q & q<s}) by A5,RCOMP_1:def 2;
then not g<x or not x<s;
hence contradiction by A4,A6,REAL_1:def 5;
end;
let x be set; assume x in ].g,s.[ \/ {g};
then A7: x in ].g,s.[ or x in {g} by XBOOLE_0:def 2;
A8: g is Real by XREAL_0:def 1;
now per cases by A7,TARSKI:def 1;
suppose x in ].g,s.[;
then x in {r where r is Real: g<r & r<s} by RCOMP_1:def 2;
then ex r be Real st x = r & g<r & r<s;
then x in {r where r is Real: g<=r & r<s};
hence x in [.g,s.[ by Def1;
suppose A9: x=g;
g in {r where r is Real: g<=r & r<s} by A1,A8;
hence x in [.g,s.[ by A9,Def1;
end; hence thesis;
end;
theorem
for g,s st g<s holds ].g,s.] = ].g,s.[ \/ {s}
proof let g,s such that A1: g<s;
thus ].g,s.] c= ].g,s.[ \/ {s}
proof let x be set; assume that A2: x in ].g,s.] and
A3: not x in ].g,s.[ \/ {s};
x in {r where r is Real: g<r & r<=s} by A2,Def2;
then A4: ex r be Real st r=x & g<r & r<=s;
then reconsider x as Real;
A5: not x in ].g,s.[ & not x in {s} by A3,XBOOLE_0:def 2;
then A6: (not x in ].g,s.[) & x<> s by TARSKI:def 1;
not (x in {q where q is Real: g<q & q<s}) by A5,RCOMP_1:def 2;
then not g<x or not x<s;
hence contradiction by A4,A6,REAL_1:def 5;
end;
let x be set; assume x in ].g,s.[ \/ {s};
then A7: x in ].g,s.[ or x in {s} by XBOOLE_0:def 2;
A8: s is Real by XREAL_0:def 1;
now per cases by A7,TARSKI:def 1;
suppose x in ].g,s.[;
then x in {r where r is Real: g<r & r<s} by RCOMP_1:def 2;
then ex r be Real st x = r & g<r & r<s;
then x in {r where r is Real: g<r & r<=s};
hence x in ].g,s.] by Def2;
suppose A9: x=s;
s in {r where r is Real: g<r & r<=s} by A1,A8;
hence x in ].g,s.] by A9,Def2;
end;hence thesis;
end;
theorem
[.g,g.[ = {}
proof assume [.g,g.[ <> {};
then consider t be Real such that A1: t in [.g,g.[ by SUBSET_1:10;
t in {r where r is Real: g<=r & r<g} by A1,Def1;
then ex r be Real st r=t & g<=r & r<g;
hence contradiction;
end;
theorem
].g,g.] = {}
proof assume ].g,g.] <> {};
then consider t be Real such that A1: t in ].g,g.] by SUBSET_1:10;
t in {r where r is Real: g<r & r<=g} by A1,Def2;
then ex r be Real st r=t & g<r & r<=g;
hence contradiction;
end;
theorem
p <= g implies [.g,p.[ = {}
proof assume that A1: p <= g and A2: [.g,p.[ <> {};
consider t be Real such that A3: t in [.g,p.[ by A2,SUBSET_1:10;
t in {r where r is Real: g<=r & r<p} by A3,Def1;
then ex r be Real st r=t & g<=r & r<p;
hence contradiction by A1,AXIOMS:22;
end;
theorem
p <= g implies ].g,p.] = {}
proof assume that A1: p <= g and A2: ].g,p.] <> {};
consider t be Real such that A3: t in ].g,p.] by A2,SUBSET_1:10;
t in {r where r is Real: g<r & r<=p} by A3,Def2;
then ex r be Real st r=t & g<r & r<=p;
hence contradiction by A1,AXIOMS:22;
end;
theorem
g <= p & p<=h implies [.g,p.[ \/ [.p,h.[ = [.g,h.[
proof assume that A1: g <= p and A2: p<=h;
thus [.g,p.[ \/ [.p,h.[ c= [.g,h.[
proof let x be set;assume A3:x in [.g,p.[ \/ [.p,h.[;
now per cases by A3,XBOOLE_0:def 2;
case A4: x in [.g,p.[;
then reconsider x2=x as Real;
g<=x2 & x2<p by A4,Th3;
then g<=x2 & x2<h by A2,AXIOMS:22;
hence x in [.g,h.[ by Th3;
case A5: x in [.p,h.[;
then reconsider x2=x as Real;
p<=x2 & x2<h by A5,Th3;
then g<=x2 & x2<h by A1,AXIOMS:22;
hence x in [.g,h.[ by Th3;
end;
hence x in [.g,h.[;
end;
let x be set;assume A6: x in [.g,h.[;
then reconsider x2=x as Real;
A7: g<=x2 & x2<h by A6,Th3;
now per cases;
case x2<p;
hence x in [.g,p.[ or x in [.p,h.[ by A7,Th3;
case x2>=p;
hence x in [.g,p.[ or x in [.p,h.[ by A7,Th3;
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem
g <= p & p<=h implies ].g,p.] \/ ].p,h.] = ].g,h.]
proof assume that A1: g <= p and A2: p<=h;
thus ].g,p.] \/ ].p,h.] c= ].g,h.]
proof let x be set;assume A3:x in ].g,p.] \/ ].p,h.];
now per cases by A3,XBOOLE_0:def 2;
case A4: x in ].g,p.];
then reconsider x2=x as Real;
g<x2 & x2<=p by A4,Th4;
then g<x2 & x2<=h by A2,AXIOMS:22;
hence x in ].g,h.] by Th4;
case A5: x in ].p,h.];
then reconsider x2=x as Real;
p<x2 & x2<=h by A5,Th4;
then g<x2 & x2<=h by A1,AXIOMS:22;
hence x in ].g,h.] by Th4;
end;
hence x in ].g,h.];
end;
let x be set;assume A6: x in ].g,h.];
then reconsider x2=x as Real;
A7: g<x2 & x2<=h by A6,Th4;
now per cases;
case x2<=p;
hence x in ].g,p.] or x in ].p,h.] by A7,Th4;
case x2>p;
hence x in ].g,p.] or x in ].p,h.] by A7,Th4;
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem g<=p1 & g<=p2 & p1<=h & p2<=h implies
[.g,h.] = [.g,p1.[ \/ [.p1,p2.] \/ ].p2,h.]
proof assume A1: g<=p1 & g<=p2 & p1<=h & p2<=h;
thus [.g,h.] c= [.g,p1.[ \/ [.p1,p2.] \/ ].p2,h.]
proof let x be set;assume A2: x in [.g,h.];
then reconsider x2=x as Real;
A3: g<=x2 & x2<=h by A2,TOPREAL5:1;
now per cases;
case x2<p1;
hence x in [.g,p1.[ or x in [.p1,p2.] or x in ].p2,h.] by A3,Th3;
case A4: p1<=x2;
now per cases;
case x2<=p2;
hence x in [.g,p1.[ or x in [.p1,p2.] or x in ].p2,h.]
by A4,TOPREAL5:1;
case p2<x2;
hence x in [.g,p1.[ or x in [.p1,p2.] or x in ].p2,h.] by A3,Th4;
end;
hence x in [.g,p1.[ or x in [.p1,p2.] or x in ].p2,h.];
end;
then x in [.g,p1.[ \/ [.p1,p2.] or x in ].p2,h.] by XBOOLE_0:def 2;
hence x in [.g,p1.[ \/ [.p1,p2.] \/ ].p2,h.] by XBOOLE_0:def 2;
end;
let x be set;assume x in [.g,p1.[ \/ [.p1,p2.] \/ ].p2,h.];
then A5: x in [.g,p1.[ \/ [.p1,p2.] or x in ].p2,h.] by XBOOLE_0:def 2;
now per cases by A5,XBOOLE_0:def 2;
case A6: x in [.g,p1.[;
then reconsider x2=x as Real;
A7: g<=x2 & x2<p1 by A6,Th3;
then x2<h by A1,AXIOMS:22;
hence x in [.g,h.] by A7,TOPREAL5:1;
case A8: x in [.p1,p2.];
then reconsider x2=x as Real;
A9: p1<=x2 & x2<=p2 by A8,TOPREAL5:1;
then A10: x2<=h by A1,AXIOMS:22;
g<=x2 by A1,A9,AXIOMS:22;
hence x in [.g,h.] by A10,TOPREAL5:1;
case A11: x in ].p2,h.];
then reconsider x2=x as Real;
A12: p2<x2 & x2<=h by A11,Th4;
then g<x2 by A1,AXIOMS:22;
hence x in [.g,h.] by A12,TOPREAL5:1;
end;
hence x in [.g,h.];
end;
theorem g<p1 & g<p2 & p1<h & p2<h implies
].g,h.[ = ].g,p1.] \/ ].p1,p2.[ \/ [.p2,h.[
proof assume A1: g<p1 & g<p2 & p1<h & p2<h;
thus ].g,h.[ c= ].g,p1.] \/ ].p1,p2.[ \/ [.p2,h.[
proof let x be set;assume A2: x in ].g,h.[;
then reconsider x2=x as Real;
A3: g<x2 & x2<h by A2,JORDAN6:45;
now per cases;
case x2<=p1;
hence x in ].g,p1.] or x in ].p1,p2.[ or x in [.p2,h.[ by A3,Th4;
case A4: p1<x2;
now per cases;
case x2<p2;
hence x in ].g,p1.] or x in ].p1,p2.[ or x in [.p2,h.[
by A4,JORDAN6:45;
case p2<=x2;
hence x in ].g,p1.] or x in ].p1,p2.[ or x in [.p2,h.[ by A3,Th3;
end;
hence x in ].g,p1.] or x in ].p1,p2.[ or x in [.p2,h.[;
end;
then x in ].g,p1.] \/ ].p1,p2.[ or x in [.p2,h.[ by XBOOLE_0:def 2;
hence x in ].g,p1.] \/ ].p1,p2.[ \/ [.p2,h.[ by XBOOLE_0:def 2;
end;
let x be set;assume x in ].g,p1.] \/ ].p1,p2.[ \/ [.p2,h.[;
then A5: x in ].g,p1.] \/ ].p1,p2.[ or x in [.p2,h.[ by XBOOLE_0:def 2;
now per cases by A5,XBOOLE_0:def 2;
case A6: x in ].g,p1.];
then reconsider x2=x as Real;
A7: g<x2 & x2<=p1 by A6,Th4;
then x2<h by A1,AXIOMS:22;
hence x in ].g,h.[ by A7,JORDAN6:45;
case A8: x in ].p1,p2.[;
then reconsider x2=x as Real;
A9: p1<x2 & x2<p2 by A8,JORDAN6:45;
then A10: x2<h by A1,AXIOMS:22;
g<x2 by A1,A9,AXIOMS:22;
hence x in ].g,h.[ by A10,JORDAN6:45;
case A11: x in [.p2,h.[;
then reconsider x2=x as Real;
A12: p2<=x2 & x2<h by A11,Th3;
then g<x2 by A1,AXIOMS:22;
hence x in ].g,h.[ by A12,JORDAN6:45;
end;
hence x in ].g,h.[;
end;
theorem [.q1,q2.[ /\ [.p1,p2.[ = [.max(q1,p1),min(q2,p2).[
proof
thus [.q1,q2.[ /\ [.p1,p2.[ c= [.max(q1,p1),min(q2,p2).[
proof let x be set;assume
A1: x in [.q1,q2.[ /\ [.p1,p2.[;
then reconsider x2=x as Real;
A2: x in [.q1,q2.[ & x in [.p1,p2.[ by A1,XBOOLE_0:def 3;
then A3: q1<=x2 & x2<q2 by Th3;
A4: p1<=x2 & x2<p2 by A2,Th3;
then A5: max(q1,p1)<=x2 by A3,SQUARE_1:50;
x2<min(q2,p2) by A3,A4,JGRAPH_3:6;
hence x in [.max(q1,p1),min(q2,p2).[ by A5,Th3;
end;
let x be set;assume A6: x in [.max(q1,p1),min(q2,p2).[;
then reconsider x2=x as Real;
A7: max(q1,p1)<=x2 & x2<min(q2,p2) by A6,Th3;
then A8: q1<=x2 & p1<=x2 by SQUARE_1:50;
A9: x2<q2 & x2<p2 by A7,JGRAPH_3:6;
then A10: x in [.q1,q2.[ by A8,Th3;
x in [.p1,p2.[ by A8,A9,Th3;
hence thesis by A10,XBOOLE_0:def 3;
end;
theorem ].q1,q2.] /\ ].p1,p2.] = ].max(q1,p1),min(q2,p2).]
proof
thus ].q1,q2.] /\ ].p1,p2.] c= ].max(q1,p1),min(q2,p2).]
proof let x be set;assume
A1: x in ].q1,q2.] /\ ].p1,p2.];
then reconsider x2=x as Real;
A2: x in ].q1,q2.] & x in ].p1,p2.] by A1,XBOOLE_0:def 3;
then A3: q1<x2 & x2<=q2 by Th4;
A4: p1<x2 & x2<=p2 by A2,Th4;
then A5: max(q1,p1)<x2 by A3,Th2;
x2<=min(q2,p2) by A3,A4,SQUARE_1:39;
hence x in ].max(q1,p1),min(q2,p2).] by A5,Th4;
end;
let x be set;assume A6: x in ].max(q1,p1),min(q2,p2).];
then reconsider x2=x as Real;
A7: max(q1,p1)<x2 & x2<=min(q2,p2) by A6,Th4;
then A8: q1<x2 & p1<x2 by Th2;
A9: x2<=q2 & x2<=p2 by A7,SQUARE_1:39;
then A10: x in ].q1,q2.] by A8,Th4;
x in ].p1,p2.] by A8,A9,Th4;
hence thesis by A10,XBOOLE_0:def 3;
end;
theorem ].p,q.[ c= [.p,q.[ & ].p,q.[ c= ].p,q.]
& [.p,q.[ c= [.p,q.] & ].p,q.] c= [.p,q.]
proof
thus ].p,q.[ c= [.p,q.[
proof let x be set;assume A1: x in ].p,q.[;
then reconsider x2=x as Real;
p<x2 & x2<q by A1,JORDAN6:45;
hence x in [.p,q.[ by Th3;
end;
thus ].p,q.[ c= ].p,q.]
proof let x be set;assume A2: x in ].p,q.[;
then reconsider x2=x as Real;
p<x2 & x2<q by A2,JORDAN6:45;
hence x in ].p,q.] by Th4;
end;
thus [.p,q.[ c= [.p,q.]
proof let x be set;assume A3: x in [.p,q.[;
then reconsider x2=x as Real;
p<=x2 & x2<q by A3,Th3;
hence x in [.p,q.] by TOPREAL5:1;
end;
let x be set;assume A4: x in ].p,q.];
then reconsider x2=x as Real;
p<x2 & x2<=q by A4,Th4;
hence x in [.p,q.] by TOPREAL5:1;
end;
theorem
r in [.p,g.[ & s in [.p,g.[ implies [.r,s.] c= [.p,g.[
proof assume A1: r in [.p,g.[ & s in [.p,g.[;
then A2: p<=r & r<g by Th3;
A3: p<=s & s<g by A1,Th3;
let x be set;assume
A4: x in [.r,s.];
then reconsider x2=x as Real;
r<=x2 & x2<=s by A4,TOPREAL5:1;
then p<=x2 & x2<g by A2,A3,AXIOMS:22;
hence x in [.p,g.[ by Th3;
end;
theorem
r in ].p,g.] & s in ].p,g.] implies [.r,s.] c= ].p,g.]
proof assume A1: r in ].p,g.] & s in ].p,g.];
then A2: p<r & r<=g by Th4;
A3: p<s & s<=g by A1,Th4;
let x be set;assume
A4: x in [.r,s.];
then reconsider x2=x as Real;
r<=x2 & x2<=s by A4,TOPREAL5:1;
then p<x2 & x2<=g by A2,A3,AXIOMS:22;
hence x in ].p,g.] by Th4;
end;
theorem p<=q & q<=r implies [.p,q.] \/ ].q,r.] = [.p,r.]
proof assume A1: p<=q & q<=r;
thus [.p,q.] \/ ].q,r.] c= [.p,r.]
proof let x be set;assume
A2: x in [.p,q.] \/ ].q,r.];
now per cases by A2,XBOOLE_0:def 2;
case A3: x in [.p,q.];
then reconsider x2=x as Real;
p<=x2 & x2<=q by A3,TOPREAL5:1;
then p<=x2 & x2<=r by A1,AXIOMS:22;
hence x in [.p,r.] by TOPREAL5:1;
case A4: x in ].q,r.];
then reconsider x2=x as Real;
q<x2 & x2<=r by A4,Th4;
then p<=x2 & x2<=r by A1,AXIOMS:22;
hence x in [.p,r.] by TOPREAL5:1;
end;
hence x in [.p,r.];
end;
let x be set;assume A5: x in [.p,r.];
then reconsider x2=x as Real;
A6: p<=x2 & x2<=r by A5,TOPREAL5:1;
now per cases;
case x2<=q;
hence x in [.p,q.] or x in ].q,r.] by A6,TOPREAL5:1;
case x2>q;
hence x in [.p,q.] or x in ].q,r.] by A6,Th4;
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem p<=q & q<=r implies [.p,q.[ \/ [.q,r.] = [.p,r.]
proof assume A1: p<=q & q<=r;
thus [.p,q.[ \/ [.q,r.] c= [.p,r.]
proof let x be set;assume
A2: x in [.p,q.[ \/ [.q,r.];
now per cases by A2,XBOOLE_0:def 2;
case A3: x in [.p,q.[;
then reconsider x2=x as Real;
p<=x2 & x2<q by A3,Th3;
then p<=x2 & x2<=r by A1,AXIOMS:22;
hence x in [.p,r.] by TOPREAL5:1;
case A4: x in [.q,r.];
then reconsider x2=x as Real;
q<=x2 & x2<=r by A4,TOPREAL5:1;
then p<=x2 & x2<=r by A1,AXIOMS:22;
hence x in [.p,r.] by TOPREAL5:1;
end;
hence x in [.p,r.];
end;
let x be set;assume A5: x in [.p,r.];
then reconsider x2=x as Real;
A6: p<=x2 & x2<=r by A5,TOPREAL5:1;
now per cases;
case x2<q;
hence x in [.p,q.[ or x in [.q,r.] by A6,Th3;
case x2>=q;
hence x in [.p,q.[ or x in [.q,r.] by A6,TOPREAL5:1;
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th22: [.q1,q2.[ meets [.p1,p2.[ implies q2>=p1
proof assume [.q1,q2.[ meets [.p1,p2.[;
then consider x being set such that
A1: x in [.q1,q2.[ & x in [.p1,p2.[ by XBOOLE_0:3;
reconsider x2=x as Real by A1;
A2: q1<=x2 & x2<q2 by A1,Th3;
p1<=x2 & x2<p2 by A1,Th3;
hence thesis by A2,AXIOMS:22;
end;
theorem Th23: ].q1,q2.] meets ].p1,p2.] implies q2>=p1
proof assume ].q1,q2.] meets ].p1,p2.];
then consider x being set such that
A1: x in ].q1,q2.] & x in ].p1,p2.] by XBOOLE_0:3;
reconsider x2=x as Real by A1;
A2: q1<x2 & x2<=q2 by A1,Th4;
p1<x2 & x2<=p2 by A1,Th4;
hence thesis by A2,AXIOMS:22;
end;
theorem [.q1,q2.[ meets [.p1,p2.[ implies
[.q1,q2.[ \/ [.p1,p2.[ = [.min(q1,p1),max(q2,p2).[
proof assume A1: [.q1,q2.[ meets [.p1,p2.[;
then A2: q2>=p1 by Th22;
A3: p2>=q1 by A1,Th22;
thus [.q1,q2.[ \/ [.p1,p2.[ c= [.min(q1,p1),max(q2,p2).[
proof let x be set;assume A4:x in [.q1,q2.[ \/ [.p1,p2.[;
now per cases by A4,XBOOLE_0:def 2;
case A5: x in [.q1,q2.[;
then reconsider x2=x as Real;
A6: q1<=x2 & x2<q2 by A5,Th3;
A7: min(q1,p1)<=q1 by SQUARE_1:35;
q2<=max(q2,p2) by SQUARE_1:46;
then min(q1,p1)<=x2 & x2<max(q2,p2) by A6,A7,AXIOMS:22;
hence x in [.min(q1,p1),max(q2,p2).[ by Th3;
case A8: x in [.p1,p2.[;
then reconsider x2=x as Real;
A9: p1<=x2 & x2<p2 by A8,Th3;
A10: min(q1,p1)<=p1 by SQUARE_1:35;
p2<=max(q2,p2) by SQUARE_1:46;
then min(q1,p1)<=x2 & x2<max(q2,p2) by A9,A10,AXIOMS:22;
hence x in [.min(q1,p1),max(q2,p2).[ by Th3;
end;
hence x in [.min(q1,p1),max(q2,p2).[;
end;
let x be set;assume A11: x in [.min(q1,p1),max(q2,p2).[;
then reconsider x2=x as Real;
now per cases by SQUARE_1:38;
case A12: min(q1,p1)=q1;
then A13: q1<=x2 by A11,Th3;
now per cases by SQUARE_1:49;
case max(q2,p2)=q2;
hence x in [.q1,q2.[ or x in [.p1,p2.[ by A11,A12;
case max(q2,p2)=p2;
then A14: x2<p2 by A11,Th3;
q2<=x2 implies p1<=x2 by A2,AXIOMS:22;
hence x in [.q1,q2.[ or x in [.p1,p2.[ by A13,A14,Th3;
end;
hence x in [.q1,q2.[ or x in [.p1,p2.[;
case A15: min(q1,p1)=p1;
then A16: p1<=x2 by A11,Th3;
now per cases by SQUARE_1:49;
case max(q2,p2)=p2;
hence x in [.q1,q2.[ or x in [.p1,p2.[ by A11,A15;
case max(q2,p2)=q2;
then A17: x2<q2 by A11,Th3;
p2<=x2 implies q1<=x2 by A3,AXIOMS:22;
hence x in [.q1,q2.[ or x in [.p1,p2.[ by A16,A17,Th3;
end;
hence x in [.q1,q2.[ or x in [.p1,p2.[;
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem ].q1,q2.] meets ].p1,p2.] implies
].q1,q2.] \/ ].p1,p2.] = ].min(q1,p1),max(q2,p2).]
proof assume A1: ].q1,q2.] meets ].p1,p2.];
then A2: q2>=p1 by Th23;
A3: p2>=q1 by A1,Th23;
thus ].q1,q2.] \/ ].p1,p2.] c= ].min(q1,p1),max(q2,p2).]
proof let x be set;assume A4:x in ].q1,q2.] \/ ].p1,p2.];
now per cases by A4,XBOOLE_0:def 2;
case A5: x in ].q1,q2.];
then reconsider x2=x as Real;
A6: q1<x2 & x2<=q2 by A5,Th4;
A7: min(q1,p1)<=q1 by SQUARE_1:35;
q2<=max(q2,p2) by SQUARE_1:46;
then min(q1,p1)<x2 & x2<=max(q2,p2) by A6,A7,AXIOMS:22;
hence x in ].min(q1,p1),max(q2,p2).] by Th4;
case A8: x in ].p1,p2.];
then reconsider x2=x as Real;
A9: p1<x2 & x2<=p2 by A8,Th4;
A10: min(q1,p1)<=p1 by SQUARE_1:35;
p2<=max(q2,p2) by SQUARE_1:46;
then min(q1,p1)<x2 & x2<=max(q2,p2) by A9,A10,AXIOMS:22;
hence x in ].min(q1,p1),max(q2,p2).] by Th4;
end;
hence x in ].min(q1,p1),max(q2,p2).];
end;
let x be set;assume A11: x in ].min(q1,p1),max(q2,p2).];
then reconsider x2=x as Real;
now per cases by SQUARE_1:38;
case A12: min(q1,p1)=q1;
then A13: q1<x2 by A11,Th4;
now per cases by SQUARE_1:49;
case max(q2,p2)=q2;
hence x in ].q1,q2.] or x in ].p1,p2.] by A11,A12;
case max(q2,p2)=p2;
then A14: x2<=p2 by A11,Th4;
q2<x2 implies p1<x2 by A2,AXIOMS:22;
hence x in ].q1,q2.] or x in ].p1,p2.] by A13,A14,Th4;
end;
hence x in ].q1,q2.] or x in ].p1,p2.];
case A15: min(q1,p1)=p1;
then A16: p1<x2 by A11,Th4;
now per cases by SQUARE_1:49;
case max(q2,p2)=p2;
hence x in ].q1,q2.] or x in ].p1,p2.] by A11,A15;
case max(q2,p2)=q2;
then A17: x2<=q2 by A11,Th4;
p2<x2 implies q1<x2 by A3,AXIOMS:22;
hence x in ].q1,q2.] or x in ].p1,p2.] by A16,A17,Th4;
end;
hence x in ].q1,q2.] or x in ].p1,p2.];
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem [.p1,p2.[ meets [.q1,q2.[ implies
[.p1,p2.[ \ [.q1,q2.[ = [.p1,q1.[ \/ [.q2,p2.[
proof assume A1: [.p1,p2.[ meets [.q1,q2.[;
then A2: p2>=q1 by Th22;
A3: q2>=p1 by A1,Th22;
thus [.p1,p2.[ \ [.q1,q2.[ c= [.p1,q1.[ \/ [.q2,p2.[
proof let x be set;assume A4: x in [.p1,p2.[ \ [.q1,q2.[;
then A5: x in [.p1,p2.[ & not x in [.q1,q2.[ by XBOOLE_0:def 4;
reconsider x2=x as Real by A4;
A6: p1<=x2 & x2<p2 by A5,Th3;
now per cases by A5,Th3;
case q1>x2; hence x in [.p1,q1.[ or x in [.q2,p2.[ by A6,Th3;
case x2>=q2; hence x in [.p1,q1.[ or x in [.q2,p2.[ by A6,Th3;
end;
hence x in [.p1,q1.[ \/ [.q2,p2.[ by XBOOLE_0:def 2;
end;
let x be set;assume A7:x in [.p1,q1.[ \/ [.q2,p2.[;
now per cases by A7,XBOOLE_0:def 2;
case A8: x in [.p1,q1.[;
then reconsider x2=x as Real;
A9: p1<=x2 & x2<q1 by A8,Th3;
then x2<p2 by A2,AXIOMS:22;
hence x in [.p1,p2.[ & not x in [.q1,q2.[ by A9,Th3;
case A10: x in [.q2,p2.[;
then reconsider x2=x as Real;
A11: q2<=x2 & x2<p2 by A10,Th3;
then p1<=x2 & x2<p2 by A3,AXIOMS:22;
hence x in [.p1,p2.[ & not x in [.q1,q2.[ by A11,Th3;
end;
hence thesis by XBOOLE_0:def 4;
end;
theorem ].p1,p2.] meets ].q1,q2.] implies
].p1,p2.] \ ].q1,q2.] = ].p1,q1.] \/ ].q2,p2.]
proof assume A1: ].p1,p2.] meets ].q1,q2.];
then A2: p2>=q1 by Th23;
A3: q2>=p1 by A1,Th23;
thus ].p1,p2.] \ ].q1,q2.] c= ].p1,q1.] \/ ].q2,p2.]
proof let x be set;assume A4: x in ].p1,p2.] \ ].q1,q2.];
then A5: x in ].p1,p2.] & not x in ].q1,q2.] by XBOOLE_0:def 4;
reconsider x2=x as Real by A4;
A6: p1<x2 & x2<=p2 by A5,Th4;
now per cases by A5,Th4;
case q1>=x2;
hence x in ].p1,q1.] or x in ].q2,p2.] by A6,Th4;
case x2>q2;
hence x in ].p1,q1.] or x in ].q2,p2.] by A6,Th4;
end;
hence x in ].p1,q1.] \/ ].q2,p2.] by XBOOLE_0:def 2;
end;
let x be set;assume A7:x in ].p1,q1.] \/ ].q2,p2.];
now per cases by A7,XBOOLE_0:def 2;
case A8: x in ].p1,q1.];
then reconsider x2=x as Real;
A9: p1<x2 & x2<=q1 by A8,Th4;
then x2<=p2 by A2,AXIOMS:22;
hence x in ].p1,p2.] & not x in ].q1,q2.] by A9,Th4;
case A10: x in ].q2,p2.];
then reconsider x2=x as Real;
A11: q2<x2 & x2<=p2 by A10,Th4;
then p1<x2 & x2<=p2 by A3,AXIOMS:22;
hence x in ].p1,p2.] & not x in ].q1,q2.] by A11,Th4;
end;
hence thesis by XBOOLE_0:def 4;
end;