:: The Ordering of Points on a Curve, Part {III}
:: by Artur Korni{\l}owicz
::
:: Received September 16, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, TOPREAL2, PRE_TOPC, EUCLID, SUBSET_1, TOPREAL1, FUNCT_1,
BORSUK_1, RELAT_1, REAL_1, TOPS_2, CARD_1, XXREAL_0, STRUCT_0, XXREAL_1,
JORDAN3, PSCOMP_1, JORDAN6, ARYTM_3, XBOOLE_0, JORDAN17;
notations ORDINAL1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, RCOMP_1, STRUCT_0,
RELAT_1, FUNCT_1, TOPREAL1, TOPREAL2, PRE_TOPC, TOPS_2, BORSUK_1, EUCLID,
JORDAN5C, PSCOMP_1, JORDAN6, XXREAL_0;
constructors REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, PSCOMP_1,
JORDAN5C, JORDAN6, COMPLEX1;
registrations RELSET_1, XREAL_0, MEMBERED, TOPREAL2, EUCLID;
requirements NUMERALS, REAL, SUBSET;
definitions TOPREAL1;
equalities STRUCT_0;
theorems XBOOLE_0, JORDAN5C, JORDAN6, JORDAN7, TOPS_2, FUNCT_1, BORSUK_1,
PRE_TOPC, TOPREAL5, SPRECT_1, JORDAN16, XREAL_1, XXREAL_0, XXREAL_1;
begin
reserve C, P for Simple_closed_curve,
a, b, c, d, e for Point of TOP-REAL 2;
theorem Th1:
for n being Element of NAT, a, p1, p2 being Point of TOP-REAL n,
P being Subset of TOP-REAL n st a in P & P is_an_arc_of p1,p2 ex f being
Function of I[01], (TOP-REAL n)|P, r being Real st f is being_homeomorphism & f
.0 = p1 & f.1 = p2 & 0 <= r & r <= 1 & f.r = a
proof
let n be Element of NAT, a, p1, p2 be Point of TOP-REAL n, P be Subset of
TOP-REAL n such that
A1: a in P;
given f being Function of I[01], (TOP-REAL n)|P such that
A2: f is being_homeomorphism and
A3: f.0 = p1 & f.1 = p2;
rng f = [#]((TOP-REAL n)|P) by A2,TOPS_2:def 5
.= the carrier of (TOP-REAL n)|P
.= P by PRE_TOPC:8;
then consider r being object such that
A4: r in dom f and
A5: a = f.r by A1,FUNCT_1:def 3;
A6: dom f = [#]I[01] by A2,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
then reconsider r as Real by A4;
take f, r;
thus f is being_homeomorphism & f.0 = p1 & f.1 = p2 by A2,A3;
thus 0 <= r & r <= 1 by A4,A6,XXREAL_1:1;
thus thesis by A5;
end;
theorem
LE W-min(P),E-max(P),P
proof
A1: E-max(P) <> W-min(P) by TOPREAL5:19;
W-min(P) in Upper_Arc(P) & E-max(P) in Lower_Arc(P) by JORDAN7:1;
hence thesis by A1,JORDAN6:def 10;
end;
theorem
LE a,E-max(P),P implies a in Upper_Arc(P)
proof
assume
A1: LE a,E-max(P),P;
per cases by A1,JORDAN6:def 10;
suppose
a in Upper_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P) =
W-min(P) or a in Upper_Arc(P) & E-max(P) in Upper_Arc(P) & LE a,E-max(P),
Upper_Arc(P),W-min(P),E-max(P);
hence thesis;
end;
suppose that
A2: a in Lower_Arc(P) and
E-max(P) in Lower_Arc(P) & not E-max(P) = W-min(P) and
A3: LE a,E-max(P),Lower_Arc(P),E-max(P),W-min(P);
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by JORDAN6:def 9;
then consider
f being Function of I[01], (TOP-REAL 2)|Lower_Arc(P), r being
Real such that
A4: f is being_homeomorphism and
A5: f.0 = E-max(P) and
A6: f.1 = W-min(P) and
A7: 0 <= r and
A8: r <= 1 and
A9: f.r = a by A2,Th1;
thus thesis
proof
per cases;
suppose
r = 0;
hence thesis by A5,A9,JORDAN7:1;
end;
suppose
r <> 0;
then r > 0 by A7,XXREAL_0:1;
hence thesis by A3,A4,A5,A6,A8,A9,JORDAN5C:def 3;
end;
end;
end;
end;
theorem
LE E-max(P),a,P implies a in Lower_Arc(P)
proof
assume
A1: LE E-max(P),a,P;
per cases by A1,JORDAN6:def 10;
suppose
E-max(P) in Upper_Arc(P) & a in Lower_Arc(P) & not a = W-min(P) or
E-max(P) in Lower_Arc(P) & a in Lower_Arc(P) & not a = W-min(P) & LE E-max(P),a
,Lower_Arc(P),E-max(P),W-min(P);
hence thesis;
end;
suppose that
E-max(P) in Upper_Arc(P) and
A2: a in Upper_Arc(P) and
A3: LE E-max(P),a,Upper_Arc(P),W-min(P),E-max(P);
Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8;
then consider
f being Function of I[01], (TOP-REAL 2)|Upper_Arc(P), r being
Real such that
A4: f is being_homeomorphism & f.0 = W-min(P) and
A5: f.1 = E-max(P) and
A6: 0 <= r and
A7: r <= 1 and
A8: f.r = a by A2,Th1;
thus thesis
proof
per cases;
suppose
r = 1;
hence thesis by A5,A8,JORDAN7:1;
end;
suppose
r <> 1;
then r < 1 by A7,XXREAL_0:1;
hence thesis by A3,A4,A5,A6,A8,JORDAN5C:def 3;
end;
end;
end;
end;
theorem
LE a,W-min(P),P implies a in Lower_Arc(P)
proof
assume
A1: LE a,W-min(P),P;
per cases by A1,JORDAN6:def 10;
suppose
a in Upper_Arc(P) & W-min(P) in Lower_Arc(P) & not W-min(P) =
W-min(P) or a in Lower_Arc(P) & W-min(P) in Lower_Arc(P) & not W-min(P) = W-min
(P) & LE a,W-min(P),Lower_Arc(P),E-max(P),W-min(P);
hence thesis;
end;
suppose that
A2: a in Upper_Arc(P) and
W-min(P) in Upper_Arc(P) and
A3: LE a,W-min(P),Upper_Arc(P),W-min(P),E-max(P);
Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8;
then consider
f being Function of I[01], (TOP-REAL 2)|Upper_Arc(P), r being
Real such that
A4: f is being_homeomorphism and
A5: f.0 = W-min(P) and
A6: f.1 = E-max(P) and
A7: 0 <= r and
A8: r <= 1 and
A9: f.r = a by A2,Th1;
thus thesis
proof
per cases;
suppose
r = 0;
hence thesis by A5,A9,JORDAN7:1;
end;
suppose
r <> 0;
then r > 0 by A7,XXREAL_0:1;
hence thesis by A3,A4,A5,A6,A8,A9,JORDAN5C:def 3;
end;
end;
end;
end;
theorem Th6:
for P being Subset of TOP-REAL 2 st a <> b & P is_an_arc_of c,d &
LE a,b,P,c,d holds ex e st a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d
proof
let P be Subset of TOP-REAL 2;
assume that
A1: a <> b and
A2: P is_an_arc_of c,d and
A3: LE a,b,P,c,d;
b in P by A3,JORDAN5C:def 3;
then consider
f being Function of I[01], (TOP-REAL 2)|P, rb being Real such that
A4: f is being_homeomorphism and
A5: f.0 = c & f.1 = d and
A6: 0 <= rb and
A7: rb <= 1 and
A8: f.rb = b by A2,Th1;
A9: rng f = [#]((TOP-REAL 2)|P) by A4,TOPS_2:def 5
.= the carrier of (TOP-REAL 2)|P
.= P by PRE_TOPC:8;
a in P by A3,JORDAN5C:def 3;
then consider ra being object such that
A10: ra in dom f and
A11: a = f.ra by A9,FUNCT_1:def 3;
A12: dom f = [#]I[01] by A4,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
then reconsider ra as Real by A10;
A13: 0 <= ra by A10,A12,XXREAL_1:1;
A14: ra <= 1 by A10,A12,XXREAL_1:1;
then ra <= rb by A3,A4,A5,A6,A7,A8,A11,A13,JORDAN5C:def 3;
then ra < rb by A1,A8,A11,XXREAL_0:1;
then consider re being Real such that
A15: ra < re and
A16: re < rb by XREAL_1:5;
set e = f.re;
A17: re <= 1 by A7,A16,XXREAL_0:2;
A18: 0 <= re by A13,A15,XXREAL_0:2;
then
A19: re in dom f by A12,A17,XXREAL_1:1;
then e in rng f by FUNCT_1:def 3;
then reconsider e as Point of TOP-REAL 2 by A9;
take e;
now
assume
A20: a = e or b = e;
f is one-to-one & rb in dom f by A4,A6,A7,A12,TOPS_2:def 5,XXREAL_1:1;
hence contradiction by A8,A10,A11,A15,A16,A19,A20,FUNCT_1:def 4;
end;
hence a <> e & b <> e;
thus thesis by A2,A4,A5,A6,A7,A8,A11,A13,A14,A15,A16,A18,A17,JORDAN5C:8;
end;
theorem Th7:
a in P implies ex e st a <> e & LE a,e,P
proof
assume
A1: a in P;
A2: E-max(P) <> W-min(P) by TOPREAL5:19;
A3: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by JORDAN6:def 9;
per cases;
suppose
A4: a = W-min(P);
take E-max(P);
thus thesis by A4,JORDAN7:3,SPRECT_1:14,TOPREAL5:19;
end;
suppose
A5: a <> W-min(P);
thus thesis
proof
per cases;
suppose
A6: a in Upper_Arc(P);
thus thesis
proof
per cases;
suppose
A7: a = E-max(P);
consider e such that
A8: e in Lower_Arc(P) & e <> E-max(P) & e <> W-min(P) by A3,JORDAN6:42;
take e;
thus thesis by A6,A7,A8,JORDAN6:def 10;
end;
suppose
A9: a <> E-max(P);
take E-max(P);
E-max(P) in Lower_Arc(P) by JORDAN7:1;
hence thesis by A2,A6,A9,JORDAN6:def 10;
end;
end;
end;
suppose
A10: not a in Upper_Arc(P);
Upper_Arc(P) \/ Lower_Arc(P) = P by JORDAN6:def 9;
then
A11: a in Lower_Arc(P) by A1,A10,XBOOLE_0:def 3;
then consider
f being Function of I[01], (TOP-REAL 2)|Lower_Arc(P), r being
Real such that
A12: f is being_homeomorphism and
A13: f.0 = E-max(P) and
A14: f.1 = W-min(P) and
A15: 0 <= r and
A16: r <= 1 and
A17: f.r = a by A3,Th1;
A18: f is one-to-one by A12,TOPS_2:def 5;
r < 1 by A5,A14,A16,A17,XXREAL_0:1;
then consider s being Real such that
A19: r < s and
A20: s < 1 by XREAL_1:5;
A21: dom f = [#]I[01] by A12,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
A22: rng f = [#]((TOP-REAL 2)|Lower_Arc(P)) by A12,TOPS_2:def 5
.= the carrier of (TOP-REAL 2)|Lower_Arc(P)
.= Lower_Arc(P) by PRE_TOPC:8;
A23: 0 <= s by A15,A19,XXREAL_0:2;
then
A24: s in dom f by A21,A20,XXREAL_1:1;
then
A25: f.s in rng f by FUNCT_1:def 3;
then reconsider e = f.s as Point of TOP-REAL 2 by A22;
1 in dom f by A21,XXREAL_1:1;
then
A26: e <> W-min(P) by A14,A18,A20,A24,FUNCT_1:def 4;
take e;
r in dom f by A15,A16,A21,XXREAL_1:1;
hence a <> e by A17,A18,A19,A24,FUNCT_1:def 4;
LE a,e,Lower_Arc(P),E-max(P),W-min(P) by A3,A12,A13,A14,A15,A16
,A17,A19,A20,A23,JORDAN5C:8;
hence thesis by A11,A22,A25,A26,JORDAN6:def 10;
end;
end;
end;
end;
theorem Th8:
a <> b & LE a,b,P implies ex c st c <> a & c <> b & LE a,c,P & LE c,b,P
proof
assume that
A1: a <> b and
A2: LE a,b,P;
A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8;
A4: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by JORDAN6:def 9;
per cases by A2,JORDAN6:def 10;
suppose that
A5: a in Upper_Arc(P) and
A6: b in Lower_Arc(P) and
A7: not b = W-min(P);
A8: E-max(P) in Lower_Arc(P) by JORDAN7:1;
A9: E-max(P) in Upper_Arc(P) & E-max(P) <> W-min(P) by JORDAN7:1,TOPREAL5:19;
thus thesis
proof
per cases;
suppose that
A10: a <> E-max(P) & b <> E-max(P);
take e = E-max(P);
thus a <> e & b <> e by A10;
thus thesis by A5,A6,A7,A8,A9,JORDAN6:def 10;
end;
suppose
A11: a = E-max(P);
then LE a,b,Lower_Arc(P),E-max(P),W-min(P) by A4,A6,JORDAN5C:10;
then consider e such that
A12: a <> e & b <> e and
A13: LE a,e,Lower_Arc(P),E-max(P),W-min(P) & LE e,b,Lower_Arc(P),
E-max(P),W-min(P ) by A1,A4,Th6;
take e;
thus e <> a & e <> b by A12;
e in Lower_Arc(P) & e <> W-min(P) by A4,A7,A13,JORDAN5C:def 3
,JORDAN6:55;
hence thesis by A6,A7,A8,A11,A13,JORDAN6:def 10;
end;
suppose
A14: b = E-max(P);
then LE a,b,Upper_Arc(P),W-min(P),E-max(P) by A3,A5,JORDAN5C:10;
then consider e such that
A15: a <> e & b <> e and
A16: LE a,e,Upper_Arc(P),W-min(P),E-max(P) and
LE e,b,Upper_Arc(P),W-min(P),E-max(P) by A1,A3,Th6;
take e;
thus e <> a & e <> b by A15;
e in Upper_Arc(P) by A16,JORDAN5C:def 3;
hence thesis by A5,A7,A8,A14,A16,JORDAN6:def 10;
end;
end;
end;
suppose that
A17: a in Upper_Arc(P) & b in Upper_Arc(P) and
A18: LE a,b,Upper_Arc(P),W-min(P),E-max(P);
consider e such that
A19: a <> e & b <> e and
A20: LE a,e,Upper_Arc(P),W-min(P),E-max(P) and
A21: LE e,b,Upper_Arc(P),W-min(P),E-max(P) by A1,A3,A18,Th6;
take e;
thus e <> a & e <> b by A19;
e in Upper_Arc(P) by A20,JORDAN5C:def 3;
hence thesis by A17,A20,A21,JORDAN6:def 10;
end;
suppose that
A22: a in Lower_Arc(P) & b in Lower_Arc(P) and
A23: not b = W-min(P) and
A24: LE a,b,Lower_Arc(P),E-max(P),W-min(P);
consider e such that
A25: a <> e & b <> e and
A26: LE a,e,Lower_Arc(P),E-max(P),W-min(P) and
A27: LE e,b,Lower_Arc(P),E-max(P),W-min(P) by A1,A4,A24,Th6;
take e;
thus e <> a & e <> b by A25;
A28: e in Lower_Arc(P) by A26,JORDAN5C:def 3;
e <> W-min(P) by A4,A23,A27,JORDAN6:55;
hence thesis by A22,A23,A26,A27,A28,JORDAN6:def 10;
end;
end;
definition
let P be Subset of TOP-REAL 2, a, b, c, d be Point of TOP-REAL 2;
pred a,b,c,d are_in_this_order_on P means
LE a,b,P & LE b,c,P & LE c,
d,P or LE b,c,P & LE c,d,P & LE d,a,P or LE c,d,P & LE d,a,P & LE a,b,P or LE d
,a,P & LE a,b,P & LE b,c,P;
end;
theorem
a in P implies a,a,a,a are_in_this_order_on P
by JORDAN6:56;
theorem
a,b,c,d are_in_this_order_on P implies b,c,d,a are_in_this_order_on P;
theorem
a,b,c,d are_in_this_order_on P implies c,d,a,b are_in_this_order_on P;
theorem
a,b,c,d are_in_this_order_on P implies d,a,b,c are_in_this_order_on P;
theorem
a <> b & a,b,c,d are_in_this_order_on P implies ex e st e <> a & e <>
b & a,e,b,c are_in_this_order_on P
proof
assume that
A1: a <> b and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose
A3: LE a,b,P & LE b,c,P & LE c,d,P;
then consider e such that
A4: e <> a & e <> b & LE a,e,P & LE e,b,P by A1,Th8;
take e;
thus thesis by A3,A4;
end;
suppose that
A5: LE b,c,P and
A6: LE c,d,P and
A7: LE d,a,P;
thus thesis
proof
A8: LE c,a,P by A6,A7,JORDAN6:58;
per cases;
suppose
A9: b = W-min(P);
a in P by A7,JORDAN7:5;
then consider e such that
A10: e <> a and
A11: LE a,e,P by Th7;
take e;
thus e <> a by A10;
thus e <> b by A1,A9,A11,JORDAN7:2;
thus thesis by A5,A8,A11;
end;
suppose
A12: b <> W-min(P);
take e = W-min(P);
b in P by A5,JORDAN7:5;
then
A13: LE e,b,P by JORDAN7:3;
now
LE b,d,P by A5,A6,JORDAN6:58;
then
A14: LE b,a,P by A7,JORDAN6:58;
assume e = a;
hence contradiction by A1,A13,A14,JORDAN6:57;
end;
hence e <> a;
thus e <> b by A12;
thus thesis by A5,A8,A13;
end;
end;
end;
suppose that
A15: LE c,d,P and
A16: LE d,a,P & LE a,b,P;
consider e such that
A17: e <> a & e <> b & LE a,e,P & LE e,b,P by A1,A16,Th8;
take e;
LE c,a,P by A15,A16,JORDAN6:58;
hence thesis by A17;
end;
suppose that
A18: LE d,a,P & LE a,b,P and
A19: LE b,c,P;
consider e such that
A20: e <> a & e <> b & LE a,e,P & LE e,b,P by A1,A18,Th8;
take e;
thus thesis by A19,A20;
end;
end;
theorem
a <> b & a,b,c,d are_in_this_order_on P implies ex e st e <> a & e <>
b & a,e,b,d are_in_this_order_on P
proof
assume that
A1: a <> b and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose that
A3: LE a,b,P and
A4: LE b,c,P & LE c,d,P;
consider e such that
A5: e <> a & e <> b & LE a,e,P & LE e,b,P by A1,A3,Th8;
take e;
LE b,d,P by A4,JORDAN6:58;
hence thesis by A5;
end;
suppose that
A6: LE b,c,P and
A7: LE c,d,P and
A8: LE d,a,P;
thus thesis
proof
A9: LE b,d,P by A6,A7,JORDAN6:58;
per cases;
suppose
A10: b = W-min(P);
a in P by A8,JORDAN7:5;
then consider e such that
A11: e <> a and
A12: LE a,e,P by Th7;
take e;
thus e <> a by A11;
thus e <> b by A1,A10,A12,JORDAN7:2;
thus thesis by A8,A9,A12;
end;
suppose
A13: b <> W-min(P);
take e = W-min(P);
b in P by A6,JORDAN7:5;
then
A14: LE e,b,P by JORDAN7:3;
now
LE b,d,P by A6,A7,JORDAN6:58;
then
A15: LE b,a,P by A8,JORDAN6:58;
assume e = a;
hence contradiction by A1,A14,A15,JORDAN6:57;
end;
hence e <> a;
thus e <> b by A13;
thus thesis by A8,A9,A14;
end;
end;
end;
suppose that
LE c,d,P and
A16: LE d,a,P and
A17: LE a,b,P;
consider e such that
A18: e <> a & e <> b & LE a,e,P & LE e,b,P by A1,A17,Th8;
take e;
thus thesis by A16,A18;
end;
suppose that
A19: LE d,a,P and
A20: LE a,b,P and
LE b,c,P;
consider e such that
A21: e <> a & e <> b & LE a,e,P & LE e,b,P by A1,A20,Th8;
take e;
thus thesis by A19,A21;
end;
end;
theorem
b <> c & a,b,c,d are_in_this_order_on P implies ex e st e <> b & e <>
c & a,b,e,c are_in_this_order_on P
proof
assume that
A1: b <> c and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose
A3: LE a,b,P & LE b,c,P & LE c,d,P;
then consider e such that
A4: e <> b & e <> c & LE b,e,P & LE e,c,P by A1,Th8;
take e;
thus thesis by A3,A4;
end;
suppose that
A5: LE b,c,P and
A6: LE c,d,P & LE d,a,P;
consider e such that
A7: e <> b & e <> c & LE b,e,P & LE e,c,P by A1,A5,Th8;
take e;
LE c,a,P by A6,JORDAN6:58;
hence thesis by A7;
end;
suppose that
A8: LE c,d,P and
A9: LE d,a,P and
A10: LE a,b,P;
thus thesis
proof
A11: LE c,a,P by A8,A9,JORDAN6:58;
per cases;
suppose
A12: c = W-min(P);
b in P by A10,JORDAN7:5;
then consider e such that
A13: e <> b and
A14: LE b,e,P by Th7;
take e;
thus e <> b by A13;
thus e <> c by A1,A12,A14,JORDAN7:2;
thus thesis by A10,A11,A14;
end;
suppose
A15: c <> W-min(P);
take e = W-min(P);
c in P by A8,JORDAN7:5;
then
A16: LE e,c,P by JORDAN7:3;
now
LE c,a,P by A8,A9,JORDAN6:58;
then
A17: LE c,b,P by A10,JORDAN6:58;
assume e = b;
hence contradiction by A1,A16,A17,JORDAN6:57;
end;
hence e <> b;
thus e <> c by A15;
thus thesis by A10,A11,A16;
end;
end;
end;
suppose that
LE d,a,P and
A18: LE a,b,P & LE b,c,P;
consider e such that
A19: e <> b & e <> c & LE b,e,P & LE e,c,P by A1,A18,Th8;
take e;
thus thesis by A18,A19;
end;
end;
theorem
b <> c & a,b,c,d are_in_this_order_on P implies ex e st e <> b & e <>
c & b,e,c,d are_in_this_order_on P
proof
assume that
A1: b <> c and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose
A3: LE a,b,P & LE b,c,P & LE c,d,P;
then consider e such that
A4: e <> b & e <> c & LE b,e,P & LE e,c,P by A1,Th8;
take e;
thus thesis by A3,A4;
end;
suppose
A5: LE b,c,P & LE c,d,P & LE d,a,P;
then consider e such that
A6: e <> b & e <> c & LE b,e,P & LE e,c,P by A1,Th8;
take e;
thus thesis by A5,A6;
end;
suppose that
A7: LE c,d,P and
A8: LE d,a,P and
A9: LE a,b,P;
thus thesis
proof
A10: LE d,b,P by A8,A9,JORDAN6:58;
per cases;
suppose
A11: c = W-min(P);
b in P by A9,JORDAN7:5;
then consider e such that
A12: e <> b and
A13: LE b,e,P by Th7;
take e;
thus e <> b by A12;
thus e <> c by A1,A11,A13,JORDAN7:2;
thus thesis by A7,A10,A13;
end;
suppose
A14: c <> W-min(P);
take e = W-min(P);
c in P by A7,JORDAN7:5;
then
A15: LE e,c,P by JORDAN7:3;
now
LE c,a,P by A7,A8,JORDAN6:58;
then
A16: LE c,b,P by A9,JORDAN6:58;
assume e = b;
hence contradiction by A1,A15,A16,JORDAN6:57;
end;
hence e <> b;
thus e <> c by A14;
thus thesis by A7,A10,A15;
end;
end;
end;
suppose that
A17: LE d,a,P & LE a,b,P and
A18: LE b,c,P;
consider e such that
A19: e <> b & e <> c and
A20: LE b,e,P & LE e,c,P by A1,A18,Th8;
take e;
thus e <> b & e <> c by A19;
LE d,b,P by A17,JORDAN6:58;
hence thesis by A20;
end;
end;
theorem
c <> d & a,b,c,d are_in_this_order_on P implies ex e st e <> c & e <>
d & a,c,e,d are_in_this_order_on P
proof
assume that
A1: c <> d and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose that
A3: LE a,b,P & LE b,c,P and
A4: LE c,d,P;
consider e such that
A5: e <> c & e <> d & LE c,e,P & LE e,d,P by A1,A4,Th8;
take e;
LE a,c,P by A3,JORDAN6:58;
hence thesis by A5;
end;
suppose that
A6: LE b,c,P & LE c,d,P and
A7: LE d,a,P;
consider e such that
A8: e <> c & e <> d & LE c,e,P & LE e,d,P by A1,A6,Th8;
take e;
thus thesis by A7,A8;
end;
suppose that
A9: LE c,d,P and
A10: LE d,a,P and
LE a,b,P;
consider e such that
A11: e <> c & e <> d & LE c,e,P & LE e,d,P by A1,A9,Th8;
take e;
thus thesis by A10,A11;
end;
suppose that
A12: LE d,a,P and
A13: LE a,b,P and
A14: LE b,c,P;
thus thesis
proof
A15: LE a,c,P by A13,A14,JORDAN6:58;
per cases;
suppose
A16: d = W-min(P);
c in P by A14,JORDAN7:5;
then consider e such that
A17: e <> c and
A18: LE c,e,P by Th7;
take e;
thus e <> c by A17;
thus e <> d by A1,A16,A18,JORDAN7:2;
thus thesis by A12,A15,A18;
end;
suppose
A19: d <> W-min(P);
take e = W-min(P);
d in P by A12,JORDAN7:5;
then
A20: LE e,d,P by JORDAN7:3;
now
LE d,b,P by A12,A13,JORDAN6:58;
then
A21: LE d,c,P by A14,JORDAN6:58;
assume e = c;
hence contradiction by A1,A20,A21,JORDAN6:57;
end;
hence e <> c;
thus e <> d by A19;
thus thesis by A12,A15,A20;
end;
end;
end;
end;
theorem
c <> d & a,b,c,d are_in_this_order_on P implies ex e st e <> c & e <>
d & b,c,e,d are_in_this_order_on P
proof
assume that
A1: c <> d and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose that
A3: LE a,b,P & LE b,c,P and
A4: LE c,d,P;
consider e such that
A5: e <> c & e <> d & LE c,e,P & LE e,d,P by A1,A4,Th8;
take e;
thus thesis by A3,A5;
end;
suppose that
A6: LE b,c,P and
A7: LE c,d,P and
LE d,a,P;
consider e such that
A8: e <> c & e <> d & LE c,e,P & LE e,d,P by A1,A7,Th8;
take e;
thus thesis by A6,A8;
end;
suppose that
A9: LE c,d,P and
A10: LE d,a,P & LE a,b,P;
consider e such that
A11: e <> c & e <> d & LE c,e,P & LE e,d,P by A1,A9,Th8;
take e;
LE d,b,P by A10,JORDAN6:58;
hence thesis by A11;
end;
suppose that
A12: LE d,a,P and
A13: LE a,b,P and
A14: LE b,c,P;
thus thesis
proof
A15: LE d,b,P by A12,A13,JORDAN6:58;
per cases;
suppose
A16: d = W-min(P);
c in P by A14,JORDAN7:5;
then consider e such that
A17: e <> c and
A18: LE c,e,P by Th7;
take e;
thus e <> c by A17;
thus e <> d by A1,A16,A18,JORDAN7:2;
thus thesis by A14,A15,A18;
end;
suppose
A19: d <> W-min(P);
take e = W-min(P);
d in P by A12,JORDAN7:5;
then
A20: LE e,d,P by JORDAN7:3;
now
assume
A21: e = c;
LE d,c,P by A14,A15,JORDAN6:58;
hence contradiction by A1,A20,A21,JORDAN6:57;
end;
hence e <> c;
thus e <> d by A19;
thus thesis by A14,A15,A20;
end;
end;
end;
end;
theorem
d <> a & a,b,c,d are_in_this_order_on P implies ex e st e <> d & e <>
a & a,b,d,e are_in_this_order_on P
proof
assume that
A1: d <> a and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose that
A3: LE a,b,P and
A4: LE b,c,P and
A5: LE c,d,P;
thus thesis
proof
A6: LE b,d,P by A4,A5,JORDAN6:58;
per cases;
suppose
A7: a = W-min(P);
d in P by A5,JORDAN7:5;
then consider e such that
A8: e <> d and
A9: LE d,e,P by Th7;
take e;
thus e <> d by A8;
thus e <> a by A1,A7,A9,JORDAN7:2;
thus thesis by A3,A6,A9;
end;
suppose
A10: a <> W-min(P);
take e = W-min(P);
a in P by A3,JORDAN7:5;
then
A11: LE e,a,P by JORDAN7:3;
now
LE a,c,P by A3,A4,JORDAN6:58;
then
A12: LE a,d,P by A5,JORDAN6:58;
assume e = d;
hence contradiction by A1,A11,A12,JORDAN6:57;
end;
hence e <> d;
thus e <> a by A10;
thus thesis by A3,A6,A11;
end;
end;
end;
suppose that
A13: LE b,c,P & LE c,d,P and
A14: LE d,a,P;
consider e such that
A15: e <> d & e <> a & LE d,e,P & LE e,a,P by A1,A14,Th8;
take e;
LE b,d,P by A13,JORDAN6:58;
hence thesis by A15;
end;
suppose that
LE c,d,P and
A16: LE d,a,P and
A17: LE a,b,P;
consider e such that
A18: e <> d & e <> a & LE d,e,P & LE e,a,P by A1,A16,Th8;
take e;
thus thesis by A17,A18;
end;
suppose that
A19: LE d,a,P and
A20: LE a,b,P and
LE b,c,P;
consider e such that
A21: e <> d & e <> a & LE d,e,P & LE e,a,P by A1,A19,Th8;
take e;
thus thesis by A20,A21;
end;
end;
theorem
d <> a & a,b,c,d are_in_this_order_on P implies ex e st e <> d & e <>
a & a,c,d,e are_in_this_order_on P
proof
assume that
A1: d <> a and
A2: LE a,b,P & LE b,c,P & LE c,d,P or LE b,c,P & LE c,d,P & LE d,a,P or
LE c,d,P & LE d,a,P & LE a,b,P or LE d,a,P & LE a,b,P & LE b,c,P;
per cases by A2;
suppose that
A3: LE a,b,P and
A4: LE b,c,P and
A5: LE c,d,P;
thus thesis
proof
A6: LE a,c,P by A3,A4,JORDAN6:58;
per cases;
suppose
A7: a = W-min(P);
d in P by A5,JORDAN7:5;
then consider e such that
A8: e <> d and
A9: LE d,e,P by Th7;
take e;
thus e <> d by A8;
thus e <> a by A1,A7,A9,JORDAN7:2;
thus thesis by A5,A6,A9;
end;
suppose
A10: a <> W-min(P);
take e = W-min(P);
a in P by A3,JORDAN7:5;
then
A11: LE e,a,P by JORDAN7:3;
now
assume
A12: e = d;
LE a,d,P by A5,A6,JORDAN6:58;
hence contradiction by A1,A11,A12,JORDAN6:57;
end;
hence e <> d;
thus e <> a by A10;
thus thesis by A5,A6,A11;
end;
end;
end;
suppose that
LE b,c,P and
A13: LE c,d,P and
A14: LE d,a,P;
consider e such that
A15: e <> d & e <> a & LE d,e,P & LE e,a,P by A1,A14,Th8;
take e;
thus thesis by A13,A15;
end;
suppose that
A16: LE c,d,P and
A17: LE d,a,P and
LE a,b,P;
consider e such that
A18: e <> d & e <> a & LE d,e,P & LE e,a,P by A1,A17,Th8;
take e;
thus thesis by A16,A18;
end;
suppose that
A19: LE d,a,P and
A20: LE a,b,P & LE b,c,P;
consider e such that
A21: e <> d & e <> a & LE d,e,P & LE e,a,P by A1,A19,Th8;
take e;
LE a,c,P by A20,JORDAN6:58;
hence thesis by A21;
end;
end;
theorem
a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & b,a,c,d
are_in_this_order_on P implies a = b
proof
assume that
A1: a <> c and
A2: a <> d and
A3: b <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: b,a,c,d are_in_this_order_on P;
per cases by A4;
suppose
A6: LE a,b,P & LE b,c,P & LE c,d,P;
then
A7: LE b,d,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE b,a,P & LE a,c,P & LE c,d,P;
hence thesis by A6,JORDAN6:57;
end;
suppose
LE a,c,P & LE c,d,P & LE d,b,P;
hence thesis by A3,A7,JORDAN6:57;
end;
suppose
LE c,d,P & LE d,b,P & LE b,a,P;
hence thesis by A6,JORDAN6:57;
end;
suppose
LE d,b,P & LE b,a,P & LE a,c,P;
hence thesis by A6,JORDAN6:57;
end;
end;
end;
suppose
A8: LE b,c,P & LE c,d,P & LE d,a,P;
then
A9: LE b,d,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
A10: LE b,a,P & LE a,c,P & LE c,d,P;
LE c,a,P by A8,JORDAN6:58;
hence thesis by A1,A10,JORDAN6:57;
end;
suppose
LE a,c,P & LE c,d,P & LE d,b,P;
hence thesis by A3,A9,JORDAN6:57;
end;
suppose
LE c,d,P & LE d,b,P & LE b,a,P;
hence thesis by A3,A9,JORDAN6:57;
end;
suppose
LE d,b,P & LE b,a,P & LE a,c,P;
hence thesis by A3,A9,JORDAN6:57;
end;
end;
end;
suppose
A11: LE c,d,P & LE d,a,P & LE a,b,P;
then
A12: LE c,a,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE b,a,P & LE a,c,P & LE c,d,P;
hence thesis by A11,JORDAN6:57;
end;
suppose
LE a,c,P & LE c,d,P & LE d,b,P;
hence thesis by A1,A12,JORDAN6:57;
end;
suppose
LE c,d,P & LE d,b,P & LE b,a,P;
hence thesis by A11,JORDAN6:57;
end;
suppose
LE d,b,P & LE b,a,P & LE a,c,P;
hence thesis by A11,JORDAN6:57;
end;
end;
end;
suppose
A13: LE d,a,P & LE a,b,P & LE b,c,P;
thus thesis
proof
per cases by A5;
suppose
LE b,a,P & LE a,c,P & LE c,d,P;
hence thesis by A13,JORDAN6:57;
end;
suppose
LE a,c,P & LE c,d,P & LE d,b,P;
then LE a,d,P by JORDAN6:58;
hence thesis by A2,A13,JORDAN6:57;
end;
suppose
LE c,d,P & LE d,b,P & LE b,a,P;
hence thesis by A13,JORDAN6:57;
end;
suppose
LE d,b,P & LE b,a,P & LE a,c,P;
hence thesis by A13,JORDAN6:57;
end;
end;
end;
end;
theorem
a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d
are_in_this_order_on P implies a = c
proof
assume that
A1: a <> b and
A2: b <> c and
A3: c <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: c,b,a,d are_in_this_order_on P;
per cases by A4;
suppose
A6: LE a,b,P & LE b,c,P & LE c,d,P;
thus thesis
proof
per cases by A5;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A1,A6,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A3,A6,JORDAN6:57;
end;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A3,A6,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A3,A6,JORDAN6:57;
end;
end;
end;
suppose
A7: LE b,c,P & LE c,d,P & LE d,a,P;
thus thesis
proof
per cases by A5;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A2,A7,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A3,A7,JORDAN6:57;
end;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A3,A7,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A3,A7,JORDAN6:57;
end;
end;
end;
suppose
A8: LE c,d,P & LE d,a,P & LE a,b,P;
thus thesis
proof
per cases by A5;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A1,A8,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A3,A8,JORDAN6:57;
end;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A3,A8,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A3,A8,JORDAN6:57;
end;
end;
end;
suppose
A9: LE d,a,P & LE a,b,P & LE b,c,P;
thus thesis
proof
per cases by A5;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A2,A9,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A1,A9,JORDAN6:57;
end;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A2,A9,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A1,A9,JORDAN6:57;
end;
end;
end;
end;
theorem
a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a
are_in_this_order_on P implies a = d
proof
assume that
A1: a <> b and
A2: a <> c and
A3: b <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: d,b,c,a are_in_this_order_on P;
per cases by A4;
suppose
A6: LE a,b,P & LE b,c,P & LE c,d,P;
then
A7: LE a,c,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE d,b,P & LE b,c,P & LE c,a,P;
hence thesis by A2,A7,JORDAN6:57;
end;
suppose
LE b,c,P & LE c,a,P & LE a,d,P;
hence thesis by A2,A7,JORDAN6:57;
end;
suppose
LE c,a,P & LE a,d,P & LE d,b,P;
hence thesis by A2,A7,JORDAN6:57;
end;
suppose
A8: LE a,d,P & LE d,b,P & LE b,c,P;
LE b,d,P by A6,JORDAN6:58;
hence thesis by A3,A8,JORDAN6:57;
end;
end;
end;
suppose
A9: LE b,c,P & LE c,d,P & LE d,a,P;
then
A10: LE b,d,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE d,b,P & LE b,c,P & LE c,a,P;
hence thesis by A3,A10,JORDAN6:57;
end;
suppose
LE b,c,P & LE c,a,P & LE a,d,P;
hence thesis by A9,JORDAN6:57;
end;
suppose
LE c,a,P & LE a,d,P & LE d,b,P;
hence thesis by A9,JORDAN6:57;
end;
suppose
LE a,d,P & LE d,b,P & LE b,c,P;
hence thesis by A9,JORDAN6:57;
end;
end;
end;
suppose
A11: LE c,d,P & LE d,a,P & LE a,b,P;
thus thesis
proof
per cases by A5;
suppose
LE d,b,P & LE b,c,P & LE c,a,P;
then LE b,a,P by JORDAN6:58;
hence thesis by A1,A11,JORDAN6:57;
end;
suppose
LE b,c,P & LE c,a,P & LE a,d,P;
hence thesis by A11,JORDAN6:57;
end;
suppose
LE c,a,P & LE a,d,P & LE d,b,P;
hence thesis by A11,JORDAN6:57;
end;
suppose
LE a,d,P & LE d,b,P & LE b,c,P;
hence thesis by A11,JORDAN6:57;
end;
end;
end;
suppose
A12: LE d,a,P & LE a,b,P & LE b,c,P;
thus thesis
proof
per cases by A5;
suppose
A13: LE d,b,P & LE b,c,P & LE c,a,P;
LE a,c,P by A12,JORDAN6:58;
hence thesis by A2,A13,JORDAN6:57;
end;
suppose
LE b,c,P & LE c,a,P & LE a,d,P;
hence thesis by A12,JORDAN6:57;
end;
suppose
LE c,a,P & LE a,d,P & LE d,b,P;
hence thesis by A12,JORDAN6:57;
end;
suppose
LE a,d,P & LE d,b,P & LE b,c,P;
hence thesis by A12,JORDAN6:57;
end;
end;
end;
end;
theorem
a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & a,c,b,d
are_in_this_order_on P implies b = c
proof
assume that
A1: a <> c and
A2: a <> d and
A3: b <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: a,c,b,d are_in_this_order_on P;
per cases by A4;
suppose
A6: LE a,b,P & LE b,c,P & LE c,d,P;
then
A7: LE b,d,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE a,c,P & LE c,b,P & LE b,d,P;
hence thesis by A6,JORDAN6:57;
end;
suppose
LE c,b,P & LE b,d,P & LE d,a,P;
hence thesis by A6,JORDAN6:57;
end;
suppose
A8: LE b,d,P & LE d,a,P & LE a,c,P;
LE a,d,P by A6,A7,JORDAN6:58;
hence thesis by A2,A8,JORDAN6:57;
end;
suppose
LE d,a,P & LE a,c,P & LE c,b,P;
hence thesis by A6,JORDAN6:57;
end;
end;
end;
suppose
A9: LE b,c,P & LE c,d,P & LE d,a,P;
then
A10: LE c,a,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE a,c,P & LE c,b,P & LE b,d,P;
hence thesis by A9,JORDAN6:57;
end;
suppose
LE c,b,P & LE b,d,P & LE d,a,P;
hence thesis by A9,JORDAN6:57;
end;
suppose
LE b,d,P & LE d,a,P & LE a,c,P;
hence thesis by A1,A10,JORDAN6:57;
end;
suppose
LE d,a,P & LE a,c,P & LE c,b,P;
hence thesis by A9,JORDAN6:57;
end;
end;
end;
suppose
A11: LE c,d,P & LE d,a,P & LE a,b,P;
then
A12: LE c,a,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE a,c,P & LE c,b,P & LE b,d,P;
hence thesis by A1,A12,JORDAN6:57;
end;
suppose
A13: LE c,b,P & LE b,d,P & LE d,a,P;
LE d,b,P by A11,JORDAN6:58;
hence thesis by A3,A13,JORDAN6:57;
end;
suppose
LE b,d,P & LE d,a,P & LE a,c,P;
hence thesis by A1,A12,JORDAN6:57;
end;
suppose
LE d,a,P & LE a,c,P & LE c,b,P;
hence thesis by A1,A12,JORDAN6:57;
end;
end;
end;
suppose
A14: LE d,a,P & LE a,b,P & LE b,c,P;
thus thesis
proof
per cases by A5;
suppose
LE a,c,P & LE c,b,P & LE b,d,P;
hence thesis by A14,JORDAN6:57;
end;
suppose
LE c,b,P & LE b,d,P & LE d,a,P;
hence thesis by A14,JORDAN6:57;
end;
suppose
A15: LE b,d,P & LE d,a,P & LE a,c,P;
LE d,b,P by A14,JORDAN6:58;
hence thesis by A3,A15,JORDAN6:57;
end;
suppose
LE d,a,P & LE a,c,P & LE c,b,P;
hence thesis by A14,JORDAN6:57;
end;
end;
end;
end;
theorem
a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & a,d,c,b
are_in_this_order_on P implies b = d
proof
assume that
A1: a <> b and
A2: b <> c and
A3: c <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: a,d,c,b are_in_this_order_on P;
per cases by A4;
suppose
A6: LE a,b,P & LE b,c,P & LE c,d,P;
thus thesis
proof
per cases by A5;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A2,A6,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A3,A6,JORDAN6:57;
end;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A2,A6,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A3,A6,JORDAN6:57;
end;
end;
end;
suppose
A7: LE b,c,P & LE c,d,P & LE d,a,P;
thus thesis
proof
per cases by A5;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A3,A7,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A3,A7,JORDAN6:57;
end;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A2,A7,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A3,A7,JORDAN6:57;
end;
end;
end;
suppose
A8: LE c,d,P & LE d,a,P & LE a,b,P;
thus thesis
proof
per cases by A5;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A3,A8,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A1,A8,JORDAN6:57;
end;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A1,A8,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A1,A8,JORDAN6:57;
end;
end;
end;
suppose
A9: LE d,a,P & LE a,b,P & LE b,c,P;
thus thesis
proof
per cases by A5;
suppose
LE a,d,P & LE d,c,P & LE c,b,P;
hence thesis by A2,A9,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,b,P & LE b,a,P;
hence thesis by A2,A9,JORDAN6:57;
end;
suppose
LE c,b,P & LE b,a,P & LE a,d,P;
hence thesis by A2,A9,JORDAN6:57;
end;
suppose
LE b,a,P & LE a,d,P & LE d,c,P;
hence thesis by A1,A9,JORDAN6:57;
end;
end;
end;
end;
theorem
a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c
are_in_this_order_on P implies c = d
proof
assume that
A1: a <> b and
A2: a <> c and
A3: b <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: a,b,d,c are_in_this_order_on P;
per cases by A4;
suppose
A6: LE a,b,P & LE b,c,P & LE c,d,P;
thus thesis
proof
per cases by A5;
suppose
LE a,b,P & LE b,d,P & LE d,c,P;
hence thesis by A6,JORDAN6:57;
end;
suppose
LE b,d,P & LE d,c,P & LE c,a,P;
hence thesis by A6,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,a,P & LE a,b,P;
hence thesis by A6,JORDAN6:57;
end;
suppose
A7: LE c,a,P & LE a,b,P & LE b,d,P;
LE a,c,P by A6,JORDAN6:58;
hence thesis by A2,A7,JORDAN6:57;
end;
end;
end;
suppose
A8: LE b,c,P & LE c,d,P & LE d,a,P;
then
A9: LE c,a,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE a,b,P & LE b,d,P & LE d,c,P;
hence thesis by A8,JORDAN6:57;
end;
suppose
LE b,d,P & LE d,c,P & LE c,a,P;
hence thesis by A8,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,a,P & LE a,b,P;
hence thesis by A8,JORDAN6:57;
end;
suppose
A10: LE c,a,P & LE a,b,P & LE b,d,P;
LE b,a,P by A8,A9,JORDAN6:58;
hence thesis by A1,A10,JORDAN6:57;
end;
end;
end;
suppose
A11: LE c,d,P & LE d,a,P & LE a,b,P;
then
A12: LE d,b,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE a,b,P & LE b,d,P & LE d,c,P;
hence thesis by A11,JORDAN6:57;
end;
suppose
LE b,d,P & LE d,c,P & LE c,a,P;
hence thesis by A11,JORDAN6:57;
end;
suppose
LE d,c,P & LE c,a,P & LE a,b,P;
hence thesis by A11,JORDAN6:57;
end;
suppose
LE c,a,P & LE a,b,P & LE b,d,P;
hence thesis by A3,A12,JORDAN6:57;
end;
end;
end;
suppose
A13: LE d,a,P & LE a,b,P & LE b,c,P;
then
A14: LE d,b,P by JORDAN6:58;
thus thesis
proof
per cases by A5;
suppose
LE a,b,P & LE b,d,P & LE d,c,P;
hence thesis by A3,A14,JORDAN6:57;
end;
suppose
LE b,d,P & LE d,c,P & LE c,a,P;
hence thesis by A3,A14,JORDAN6:57;
end;
suppose
A15: LE d,c,P & LE c,a,P & LE a,b,P;
LE a,c,P by A13,JORDAN6:58;
hence thesis by A2,A15,JORDAN6:57;
end;
suppose
LE c,a,P & LE a,b,P & LE b,d,P;
hence thesis by A3,A14,JORDAN6:57;
end;
end;
end;
end;
theorem
a in C & b in C & c in C & d in C implies a,b,c,d are_in_this_order_on
C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,
b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b
are_in_this_order_on C
proof
assume that
A1: a in C and
A2: b in C and
A3: c in C and
A4: d in C;
per cases;
suppose
LE a,b,C & LE b,c,C & LE c,d,C;
hence thesis;
end;
suppose
A5: LE a,b,C & LE b,c,C & not LE c,d,C;
then
A6: LE d,c,C by A3,A4,JORDAN16:7;
thus thesis
proof
per cases by A1,A4,JORDAN16:7;
suppose
A7: LE a,d,C;
LE b,d,C or LE d,b,C by A2,A4,JORDAN16:7;
hence thesis by A5,A6,A7;
end;
suppose
LE d,a,C;
hence thesis by A5;
end;
end;
end;
suppose
A8: LE a,b,C & not LE b,c,C & LE c,d,C;
then
A9: LE c,b,C by A2,A3,JORDAN16:7;
thus thesis
proof
per cases by A2,A4,JORDAN16:7;
suppose
A10: LE b,d,C;
LE a,c,C or LE c,a,C by A1,A3,JORDAN16:7;
hence thesis by A8,A9,A10;
end;
suppose
A11: LE d,b,C;
thus thesis
proof
per cases by A1,A3,JORDAN16:7;
suppose
LE a,c,C;
hence thesis by A8,A11;
end;
suppose
A12: LE c,a,C;
LE a,d,C or LE d,a,C by A1,A4,JORDAN16:7;
hence thesis by A8,A11,A12;
end;
end;
end;
end;
end;
suppose
A13: LE a,b,C & not LE b,c,C & not LE c,d,C;
then
A14: LE d,c,C by A3,A4,JORDAN16:7;
A15: LE c,b,C by A2,A3,A13,JORDAN16:7;
thus thesis
proof
per cases by A1,A3,JORDAN16:7;
suppose
A16: LE a,c,C;
LE a,d,C or LE d,a,C by A1,A4,JORDAN16:7;
hence thesis by A15,A14,A16;
end;
suppose
LE c,a,C;
hence thesis by A13,A14;
end;
end;
end;
suppose
A17: not LE a,b,C & LE b,c,C & LE c,d,C;
then
A18: LE b,a,C by A1,A2,JORDAN16:7;
thus thesis
proof
per cases by A1,A4,JORDAN16:7;
suppose
A19: LE a,d,C;
LE a,c,C or LE c,a,C by A1,A3,JORDAN16:7;
hence thesis by A17,A18,A19;
end;
suppose
LE d,a,C;
hence thesis by A17;
end;
end;
end;
suppose
A20: not LE a,b,C & LE b,c,C & not LE c,d,C;
then
A21: LE b,a,C & LE d,c,C by A1,A2,A3,A4,JORDAN16:7;
thus thesis
proof
per cases by A1,A4,JORDAN16:7;
suppose
LE a,d,C;
hence thesis by A21;
end;
suppose
A22: LE d,a,C;
A23: LE b,d,C or LE d,b,C by A2,A4,JORDAN16:7;
LE a,c,C or LE c,a,C by A1,A3,JORDAN16:7;
hence thesis by A20,A21,A22,A23;
end;
end;
end;
suppose
A24: not LE a,b,C & not LE b,c,C & LE c,d,C;
then
A25: LE b,a,C & LE c,b,C by A1,A2,A3,JORDAN16:7;
thus thesis
proof
per cases by A1,A4,JORDAN16:7;
suppose
LE a,d,C;
hence thesis by A25;
end;
suppose
A26: LE d,a,C;
LE b,d,C or LE d,b,C by A2,A4,JORDAN16:7;
hence thesis by A24,A25,A26;
end;
end;
end;
suppose
A27: not LE a,b,C & not LE b,c,C & not LE c,d,C;
then
A28: LE d,c,C by A3,A4,JORDAN16:7;
LE b,a,C & LE c,b,C by A1,A2,A3,A27,JORDAN16:7;
hence thesis by A28;
end;
end;