Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ANALOAF, DIRAF, PARSP_1, VECTSP_1, PASCH;
notation STRUCT_0, ANALOAF, DIRAF;
constructors DIRAF, XBOOLE_0;
clusters ZFMISC_1, XBOOLE_0;
theorems DIRAF, ANALOAF;
begin
reserve OAS for OAffinSpace;
reserve a,a',b,b',c,c',d,d1,d2,e1,e2,e3,e4,e5,e6,p,p',q,r,x,y,z
for Element of OAS;
definition let OAS;
attr OAS is satisfying_Int_Par_Pasch means
for a,b,c,d,p st not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a
holds Mid c,p,d;
synonym OAS satisfies_Int_Par_Pasch;
end;
definition let OAS;
attr OAS is satisfying_Ext_Par_Pasch means
for a,b,c,d,p st Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b
holds Mid p,a,d;
synonym OAS satisfies_Ext_Par_Pasch;
end;
definition let OAS;
attr OAS is satisfying_Gen_Par_Pasch means
for a,b,c,a',b',c' st
not LIN a,b,a' & a,a' '||' b,b' & a,a' '||' c,c' & Mid a,b,c & LIN a',b',c'
holds Mid a',b',c';
synonym OAS satisfies_Gen_Par_Pasch;
end;
definition let OAS;
attr OAS is satisfying_Ext_Bet_Pasch means
for a,b,c,d,x,y st Mid a,b,d & Mid b,x,c & not LIN a,b,c
holds ex y st Mid a,y,c & Mid y,x,d;
synonym OAS satisfies_Ext_Bet_Pasch;
end;
definition let OAS;
attr OAS is satisfying_Int_Bet_Pasch means
for a,b,c,d,x,y st Mid a,b,d & Mid a,x,c & not LIN a,b,c
holds ex y st Mid b,y,c & Mid x,y,d;
synonym OAS satisfies_Int_Bet_Pasch;
end;
definition let OAS;
attr OAS is Fanoian means
for a,b,c,d st a,b // c,d & a,c // b,d & not LIN a,b,c
ex x st Mid a,x,d & Mid b,x,c;
synonym OAS satisfies_Fano;
end;
canceled 6;
theorem
Th7: b,p // p,c & p<>c & b<>p implies ex d st
a,p // p,d & a,b '||' c,d & c <>d & p<>d
proof assume that A1: b,p // p,c and A2: p<>c and A3: b<>p;
A4: now assume A5: not LIN a,b,p; consider d such that
A6: a,p // p,d and A7: a,b // c,d by A1,A3,ANALOAF:def 5;
A8: now assume d=p;
then p,c // b,a by A7,DIRAF:5;
then b,p // b,a by A1,A2,DIRAF:6;
then b,p '||' b,a by DIRAF:def 4; then LIN b,p,a
by DIRAF:def 5;
hence contradiction by A5,DIRAF:36;
end;
A9: now assume d=c;
then p,d // b,p by A1,DIRAF:5;
then a,p // b,p by A6,A8,DIRAF:6;
then p,a // p,b by DIRAF:5; then p,a '||' p,b by DIRAF:def 4;
then LIN p,a,b by DIRAF:def 5;
hence contradiction by A5,DIRAF:36; end;
a,b '||' c,d by A7,DIRAF:def 4;
hence thesis by A6,A8,A9;
end;
now assume LIN a,b,p;
then LIN p,a,b by DIRAF:36; then A10: p,a '||' p,b by DIRAF:def 5;
A11: now assume p,a // p,b;
then A12: a,p // b,p by DIRAF:5;
Mid b,p,c by A1,DIRAF:def 3;
then A13: LIN b,p,c by DIRAF:34;
consider d such that
A14: Mid p,c,d and A15: c <>d by DIRAF:17;
A16: p<>d by A14,A15,DIRAF:12;
p,c // c,d by A14,DIRAF:def 3;
then p,c // b,p & p,c // p,d by A1,ANALOAF:def 5,DIRAF:5;
then b,p // p,d by A2,ANALOAF:def 5;
then A17: a,p // p,d by A3,A12,DIRAF:6;
a,p // p,c by A1,A3,A12,DIRAF:6;
then Mid a,p,c by DIRAF:def 3; then LIN a,p,c by DIRAF:34;
then LIN p,c,a & LIN p,c,b by A13,DIRAF:36;
then A18: p,c '||' a,b by DIRAF:40;
LIN p,c,c & LIN p,c,d by A14,DIRAF:34,37;
then p,c '||' c,d by DIRAF:40;
then a,b '||' c,d by A2,A18,DIRAF:28;
hence thesis by A15,A16,A17;
end;
now assume p,a // b,p; then A19: a,p // p,b by DIRAF:5;
A20: b <> c by A1,A2,ANALOAF:def 5;
Mid a,p,b & Mid b,p,c by A1,A19,DIRAF:def 3;
then LIN a,p,b & LIN b,p,c by DIRAF:34;
then LIN p,b,a & LIN p,b,b & LIN p,b,c by DIRAF:36,37;
then LIN a,b,c & LIN a,b,b by A3,DIRAF:38;
then a,b '||' c,b by DIRAF:40;
hence thesis by A3,A19,A20;
end;
hence thesis by A10,A11,DIRAF:def 4;
end;
hence thesis by A4;
end;
theorem
Th8: p,b // p,c & p<>c & b<>p implies ex d st
p,a // p,d & a,b '||' c,d & c <>d
proof assume that A1: p,b // p,c and A2: p<>c and A3: b<>p;
consider q such that A4: Mid b,p,q and A5: p<>q by DIRAF:17;
A6: b,p // p,q by A4,DIRAF:def 3;
then consider r such that A7: a,p // p,r and
A8: a,b '||' q,r and A9: q<>r and A10: r<>p by A3,A5,Th7;
b,p // c,p by A1,DIRAF:5; then p,q // c,p by A3,A6,ANALOAF:def 5;
then q,p // p,c by DIRAF:5;
then consider d such that A11: r,p // p,d and
A12: r,q '||' c,d and A13: c <>d and d<>p by A2,A5,Th7;
q,r '||' c,d by A12,DIRAF:27;
then A14: a,b '||' c,d by A8,A9,DIRAF:28;
p,r // d,p by A11,DIRAF:5; then a,p // d,p by A7,A10,DIRAF:6;
then p,a // p,d by DIRAF:5;
hence thesis by A13,A14;
end;
theorem
p,b '||' p,c & p<>b implies ex d st p,a '||' p,d & a,b '||' c,d
proof assume that A1: p,b '||' p,c and A2: p<>b;
A3: now assume A4: p<>c;
A5: now assume p,b // p,c;
then consider d such that A6: p,a // p,d &
a,b '||' c,d and c <>d by A2,A4,Th8;
p,a '||' p,d & a,b '||' c,d by A6,DIRAF:def 4;
hence thesis; end;
now assume p,b // c,p; then b,p // p,c by DIRAF:5;
then consider d such that A7: a,p // p,d &
a,b '||' c,d & c <>d & d<>p by A2,A4,Th7;
p,a // d,p & a,b '||' c,d by A7,DIRAF:5;
then p,a '||' p,d & a,b '||' c,d by DIRAF:def 4;
hence thesis; end;
hence thesis by A1,A5,DIRAF:def 4; end;
now assume A8: p=c; p,a '||' p,p & a,b '||' p,p by DIRAF:25;
hence thesis by A8; end;
hence thesis by A3;
end;
canceled;
theorem
Th11: not LIN p,a,b & LIN p,b,c & LIN p,a,d1 & LIN p,a,d2 &
a,b '||' c,d1 & a,b '||' c,d2 implies d1=d2
proof assume that A1: not LIN p,a,b and
A2: LIN p,b,c and A3: LIN p,a,d1 and A4: LIN p,a,d2 and
A5: a,b '||' c,d1 and A6: a,b '||' c,d2;
A7: LIN p,d1,a & LIN p,d2,a by A3,A4,DIRAF:36;
A8: p<>a & p<>b & a<>b by A1,DIRAF:37;
A9: now assume c =p;
then A10: p,d1 '||' a,b & p,d2 '||' a,b by A5,A6,DIRAF:27;
A11: LIN p,d1,p & LIN p,d2,p by DIRAF:37;
A12: now assume A13: p<>d1;
then LIN p,d1,b by A7,A10,DIRAF:39;
hence contradiction by A1,A7,A11,A13,DIRAF:38; end;
now assume A14: p<>d2; then LIN p,d2,b by A7,A10,DIRAF:39;
hence contradiction by A1,A7,A11,A14,DIRAF:38; end;
hence thesis by A12;
end;
now assume A15: p<>c; assume A16: d1<>d2;
A17: LIN p,a,p by DIRAF:37;
then A18: LIN d1,d2,p by A3,A4,A8,DIRAF:38;
LIN p,a,a by DIRAF:37;
then A19: LIN d1,d2,a by A3,A4,A8,DIRAF:38;
c,d1 '||' c,d2 by A5,A6,A8,DIRAF:28;
then A20: LIN c,d1,d2 by DIRAF:def 5;
then A21: LIN d1,d2,c by DIRAF:36;
LIN d1,d2,p & LIN d1,d2,c & LIN d1,d2,d1 by A3,A4,A8,A17,A20,DIRAF:36,
38;
then A22: LIN p,c,d1 by A16,DIRAF:38; LIN d1,d2,d2 by DIRAF:37;
then LIN p,c,d2 & LIN p,c,b by A2,A16,A18,A21,DIRAF:36,38;
then LIN d1,d2,b by A15,A22,DIRAF:38;
hence contradiction by A1,A16,A18,A19,DIRAF:38;
end;
hence thesis by A9;
end;
theorem
Th12: not LIN a,b,c & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 &
a,c '||' b,d2 implies d1=d2
proof assume that A1: not LIN a,b,c and A2: a,b '||' c,d1 and
A3: a,b '||' c,d2 and A4: a,c '||' b,d1 and A5: a,c '||' b,d2;
assume A6: d1<>d2; A7: a<>b & a<>c by A1,DIRAF:37;
then A8: c,d1 '||' c,d2 by A2,A3,DIRAF:28;
b,d1 '||' b,d2 by A4,A5,A7,DIRAF:28;
then A9: LIN c,d1,d2 & LIN b,d1,d2 by A8,DIRAF:def 5;
then A10: LIN d1,d2,c & LIN d1,d2,b by DIRAF:36;
LIN d1,d2,c & LIN d1,d2,d1 by A9,DIRAF:36,37;
then d1,d2 '||' c,d1 by DIRAF:40;
then A11: d1,d2 '||' a,b or c =d1 by A2,DIRAF:28;
now assume c =d1;
then c,a '||' c,b by A4,DIRAF:27;
then LIN c,a,b by DIRAF:def 5;
hence contradiction by A1,DIRAF:36; end;
then d1,d2 '||' b,a by A11,DIRAF:27;
then LIN d1,d2,a by A6,A10,DIRAF:39;
hence contradiction by A1,A6,A10,DIRAF:38;
end;
theorem
Th13: not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a
implies Mid c,p,d
proof assume that A1: not LIN p,b,c and
A2: Mid b,p,a and A3: LIN p,c,d and A4: b,c '||' d,a;
assume A5: not Mid c,p,d; then A6: d<>p & p<>c by DIRAF:14;
p,c '||' p,d by A3,DIRAF:def 5;
then A7: p,c // p,d or p,c // d,p by DIRAF:def 4;
now assume p,c // d,p; then c,p // p,d by DIRAF:5;
hence contradiction by A5,DIRAF:def 3; end;
then consider q such that A8: p,b // p,q and A9: b,c '||' d,q
and d<>q by A6,A7,Th8;
p,b '||' p,q by A8,DIRAF:def 4; then A10: LIN p,b,q by DIRAF:def 5;
LIN b,p,a by A2,DIRAF:34; then LIN p,b,a by DIRAF:36;
then a=q by A1,A3,A4,A9,A10,Th11; then b,p // p,q by A2,DIRAF:def 3;
then p,q // b,p by DIRAF:5; then p,b // b,p or p=q by A8,DIRAF:6;
then p=b or p=q by ANALOAF:def 5;
then LIN p,d,c & p,d '||' c,b by A1,A3,A9,DIRAF:27,36,37;
then LIN p,d,p & LIN p,d,c & LIN p,d,b by A6,DIRAF:37,39;
hence contradiction by A1,A6,DIRAF:38;
end;
theorem
OAS satisfies_Int_Par_Pasch
proof let a,b,c,d,p;
assume not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a;
hence thesis by Th13;
end;
theorem
Th15: Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b
implies Mid p,a,d
proof assume that A1: Mid p,b,c and A2: LIN p,a,d
and A3: a,b '||' c,d and A4: not LIN p,a,b;
A5: now assume b=c;
then LIN p,b,b & LIN p,a,a & a,b '||' b,a & a,b '||' b,d
by A3,DIRAF:24,37;
then a=d by A2,A4,Th11; hence Mid p,a,d by DIRAF:14; end;
now assume A6: b<>c; then A7: p<>c by A1,DIRAF:12;
A8: b<>a by A4,DIRAF:37;
A9: not LIN d,b,a
proof assume LIN d,b,a;
then LIN a,b,d & a,b '||' d,c by A3,DIRAF:27,36;
then LIN a,b,c by A8,DIRAF:39; then A10: LIN b,c,a by DIRAF:36;
LIN p,b,c by A1,DIRAF:34;
then LIN b,c,p & LIN b,c,b by DIRAF:36,37;
hence contradiction by A4,A6,A10,DIRAF:38; end;
then A11: d<>a by DIRAF:37; LIN d,a,p by A2,DIRAF:36;
then d,a '||' d,p by DIRAF:def 5; then a,d '||' d,p by DIRAF:27;
then consider q such that
A12: b,d '||' d,q and A13: b,a '||' p,q by A11,DIRAF:32;
A14: not LIN b,c,d
proof assume A15: LIN b,c,d;
then A16: LIN b,c,d & LIN b,c,b by DIRAF:37;
LIN c,d,b by A15,DIRAF:36; then A17: c,d '||' c,b by DIRAF:def 5;
now assume a,b '||' c,b; then b,c '||' b,a by DIRAF:27;
then LIN b,c,a by DIRAF:def 5;
hence contradiction by A6,A9,A16,DIRAF:38;
end;
then LIN p,a,c & LIN p,b,c by A1,A2,A3,A17,DIRAF:28,34;
then LIN p,c,b & LIN p,c,c & LIN p,c,a by DIRAF:36,37;
then LIN b,c,a by A7,DIRAF:38;
hence contradiction by A6,A9,A16,DIRAF:38;
end;
A18: Mid d,b,q
proof
d,b '||' d,q by A12,DIRAF:27;
then LIN d,b,q by DIRAF:def 5; then A19: LIN b,d,q by DIRAF:36;
a,b '||' q,p by A13,DIRAF:27;
then A20: c,d '||' q,p by A3,A8,DIRAF:28;
Mid c,b,p by A1,DIRAF:13;
hence Mid d,b,q by A14,A19,A20,Th13; end;
assume A21: not Mid p,a,d;
A22: d<>p
proof assume d=p;
then LIN p,b,c & p,c '||' b,a by A1,A3,DIRAF:27,34;
then LIN p,c,b & p,c '||' b,a by DIRAF:36;
then LIN p,c,p & LIN p,c,a & LIN p,c,b by A7,DIRAF:37,39;
hence contradiction by A4,A7,DIRAF:38; end;
A23: not LIN d,p,q
proof assume LIN d,p,q;
then LIN d,p,p & LIN d,p,q & LIN d,p,a by A2,DIRAF:36,37;
then A24: LIN p,q,a by A22,DIRAF:38;
A25: p,q '||' a,b by A13,DIRAF:27;
now assume p=q;
then d,b '||' d,p by A12,DIRAF:27;
then LIN d,b,p by DIRAF:def 5;
then LIN d,p,d & LIN d,p,b & LIN d,p,a by A2,DIRAF:36,37;
hence contradiction by A9,A22,DIRAF:38; end;
then p<>q & LIN p,q,p & LIN p,q,a & LIN p,q,b
by A24,A25,DIRAF:37,39;
hence contradiction by A4,DIRAF:38;
end;
now assume Mid p,d,a;
then Mid p,d,a & d,b '||' d,q by A12,DIRAF:27;
then Mid p,d,a & LIN d,b,q by DIRAF:def 5;
then Mid p,d,a & LIN d,q,b & p,q '||' b,a by A13,DIRAF:27,36;
then Mid q,d,b by A23,Th13; then Mid b,d,q by DIRAF:13;
then b=d by A18,DIRAF:18;
hence contradiction by A9,DIRAF:37; end;
then Mid a,p,d & LIN p,b,c by A1,A2,A21,DIRAF:34,35;
then Mid b,p,c by A3,A4,Th13; then p=b by A1,DIRAF:18;
hence contradiction by A4,DIRAF:37;
end;
hence thesis by A5;
end;
theorem
OAS satisfies_Ext_Par_Pasch
proof let a,b,c,d,p;
assume Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b;
hence thesis by Th15;
end;
theorem
Th17: not LIN a,b,a' & a,a' '||' b,b' & a,a' '||' c,c' & Mid a,b,c &
LIN a',b',c' implies Mid a',b',c'
proof assume that A1: not LIN a,b,a' and A2: a,a' '||' b,b' and
A3: a,a' '||' c,c' and A4: Mid a,b,c and A5: LIN a',b',c';
A6: a<>a' & a<>b & b<>a' by A1,DIRAF:37;
A7: LIN a,b,c by A4,DIRAF:34; A8: LIN b',c',a' by A5,DIRAF:36;
A9: LIN c',b',a' by A5,DIRAF:36;
A10: a<>c by A4,A6,DIRAF:12;
A11: b,b' '||' c,c' by A2,A3,A6,DIRAF:28;
A12: b=b' implies thesis
proof assume A13: b=b';
then A14: Mid a,b',c & LIN b',a',c' by A4,A5,DIRAF:36;
A15: a,a' '||' c',c by A3,DIRAF:27;
not LIN b',a,a' by A1,A13,DIRAF:36;
hence thesis by A14,A15,Th13;
end;
now assume A16: b'<>c' & a'<>b' & b<>b';
A17: not LIN b,b',a'
proof assume A18: LIN b,b',a';
then LIN b,b',a' & b,b' '||' a',a by A2,DIRAF:27;
then LIN b,b',a & LIN b,b',b by A16,DIRAF:37,39;
hence contradiction by A1,A16,A18,DIRAF:38;
end;
A19: c =c' implies thesis
proof assume A20: c =c';
A21: b',b '||' a,a' by A2,DIRAF:27;
A22: Mid c',b,a by A4,A20,DIRAF:13;
not LIN c',b',b
proof assume LIN c',b',b;
then LIN c',b',b & LIN c',b',b' by DIRAF:37;
hence contradiction by A9,A16,A17,DIRAF:38;
end;
then Mid c',b',a' by A9,A21,A22,Th15;
hence thesis by DIRAF:13;
end;
now assume A23: c <>c';
a,b '||' a,c by A7,DIRAF:def 5; then c,a '||' a,b by DIRAF:27;
then consider x such that A24: c',a '||' a,x & c',c '||' b,x
by A10,DIRAF:32;
c,c' '||' b,x by A24,DIRAF:27;
then a,c' '||' a,x & b,b' '||' b,x by A11,A23,A24,DIRAF:27,28;
then A25: LIN a,c',x & LIN b,b',x by DIRAF:def 5;
then A26: LIN x,b,b' & LIN x,a,c' by DIRAF:36;
A27: x<>b proof
assume x=b; then LIN a,b,c' & LIN a,b,a & LIN a,b,b
by A25,DIRAF:36,37;
then LIN c,c',a & LIN c,c',b by A6,A7,DIRAF:38;
then c,c' '||' a,b by DIRAF:40; then b,b' '||' a,b by A11,A23,DIRAF:28;
then a,a' '||' a,b by A2,A16,DIRAF:28;
then LIN a,a',b by DIRAF:def 5;
hence contradiction by A1,DIRAF:36; end;
A28: LIN a,x,c' by A25,DIRAF:36;
A29: x,b '||' c,c'
proof LIN b,x,b' by A25,DIRAF:36;
then b,x '||' b,b' by DIRAF:def 5;
then b,x '||' c,c' by A11,A16,DIRAF:28;
hence x,b '||' c,c' by DIRAF:27;
end;
not LIN a,x,b
proof assume LIN a,x,b; then LIN x,b,a & LIN
x,b,b by DIRAF:36,37;
then LIN b,b',a & b,b' '||' a,a' by A2,A26,A27,DIRAF:27,38;
hence contradiction by A16,A17,DIRAF:39;
end;
then Mid a,x,c' by A4,A28,A29,Th15;
then A30: Mid c',x,a by DIRAF:13;
A31: b',x '||' a,a'
proof LIN b',b,x by A25,DIRAF:36;
then b',b '||' b',x by DIRAF:def 5;
then b,b' '||' b',x by DIRAF:27;
hence b',x '||' a,a' by A2,A16,DIRAF:28;
end;
A32: x<>b'
proof assume x=b';
then LIN b',c',a & LIN b',c',b' by A25,DIRAF:36,37;
then LIN a,a',b' & a,a' '||' b',b
by A2,A8,A16,DIRAF:27,38;
then LIN a,a',b by A6,DIRAF:39;
hence contradiction by A1,DIRAF:36;
end;
not LIN c',b',x
proof assume LIN c',b',x;
then LIN b',x,c' & LIN b',x,b' & LIN b',x,b
by A25,DIRAF:36,37;
then LIN c',b',b & LIN c',b',b' by A32,DIRAF:38;
hence contradiction by A9,A16,A17,DIRAF:38;
end;
then Mid c',b',a' by A9,A30,A31,Th15;
hence thesis by DIRAF:13;
end;
hence thesis by A19;
end;
hence thesis by A12,DIRAF:14;
end;
theorem
OAS satisfies_Gen_Par_Pasch
proof let a,b,c,a',b',c';
assume not LIN a,b,a' & a,a' '||' b,b' & a,a' '||' c,c' &
Mid a,b,c & LIN a',b',c';
hence thesis by Th17;
end;
theorem
not LIN p,a,b & a,p // p,a' & b,p // p,b' & a,b '||' a',b'
implies a,b // b',a'
proof assume that A1: not LIN p,a,b and
A2: a,p // p,a' and A3: b,p // p,b' and A4: a,b '||' a',b';
a<>p by A1,DIRAF:37;
then consider q such that A5: b,p // p,q and A6: b,a // a',q
by A2,ANALOAF:def 5;
A7: not LIN p,b,a by A1,DIRAF:36;
Mid a,p,a' & Mid b,p,b' & Mid b,p,q by A2,A3,A5,DIRAF:def 3;
then LIN a,p,a' & LIN b,p,b' & LIN b,p,q by DIRAF:34;
then A8: LIN p,a,a' & LIN p,b,b' & LIN p,b,q by DIRAF:36;
b,a '||' a',b' & b,a '||' a',q by A4,A6,DIRAF:27,def 4;
then b,a // a',b' by A6,A7,A8,Th11;
hence thesis by DIRAF:5;
end;
theorem
not LIN p,a,a' & p,a // p,b & p,a' // p,b' & a,a' '||' b,b'
implies a,a' // b,b'
proof assume that A1: not LIN p,a,a' and
A2: p,a // p,b and A3: p,a' // p,b' and A4: a,a' '||' b,b';
A5: not LIN p,a',a by A1,DIRAF:36; p,a '||' p,b by A2,DIRAF:def 4;
then A6: LIN p,a,b by DIRAF:def 5; p,a' '||' p,b' by A3,DIRAF:def 4;
then A7: LIN p,a',b' by DIRAF:def 5;
A8: a',a '||' b,b' by A4,DIRAF:27;
consider c such that A9: Mid a,p,c & p<>c by DIRAF:17;
A10: a,p // p,c by A9,DIRAF:def 3;
A11: a<>p by A1,DIRAF:37;
then consider c' such that A12: a',p // p,c' and
A13: a',a // c,c' by A10,ANALOAF:def 5;
A14: c <>c'
proof assume c =c'; then Mid a',p,c by A12,DIRAF:def 3;
then LIN a',p,c by DIRAF:34;
then LIN a,p,c & LIN p,c,a' by A9,DIRAF:34,36;
then LIN p,c,p & LIN p,c,a & LIN p,c,a' by DIRAF:36,37;
hence contradiction by A1,A9,DIRAF:38;
end;
A15: p<>c'
proof assume p=c'; then a',a '||' c,p by A13,DIRAF:def 4;
then a,p '||' p,c & p,c '||' a,a' by A10,DIRAF:27,def 4;
then a,p '||' a,a' by A9,DIRAF:28; then LIN a,p,a' by DIRAF:def 5;
hence contradiction by A1,DIRAF:36; end;
p,a // c,p by A10,DIRAF:5; then c,p // p,b by A2,A11,ANALOAF:def 5;
then consider b'' be Element of OAS such that
A16: c',p // p,b'' and A17: c',c // b,b'' by A9,ANALOAF:def 5;
a',p '||' p,c' by A12,DIRAF:def 4;
then p,a' '||' p,c' & c',p '||' p,b'' by A16,DIRAF:27,def 4;
then p,a' '||' p,c' & p,c' '||' p,b'' by DIRAF:27;
then p,a' '||' p,b'' by A15,DIRAF:28;
then A18: LIN p,a',b'' by DIRAF:def 5;
a',a '||' c',c & c',c '||' b,b'' by A13,A17,DIRAF:def 4;
then a',a '||' b,b'' by A14,DIRAF:28;
then c',c // a,a' & c',c // b,b' by A5,A6,A7,A8,A13,A17,A18,Th11,DIRAF:5
;
hence a,a' // b,b' by A14,ANALOAF:def 5;
end;
theorem
Th21: not LIN p,a,b & p,a '||' b,c & p,b '||' a,c implies
p,a // b,c & p,b // a,c
proof assume A1: not LIN p,a,b & p,a '||' b,c & p,b '||' a,c;
consider d such that
A2: p,a // b,d and A3: p,b // a,d and a<>d by ANALOAF:def 5;
p,a '||' b,d & p,b '||' a,d by A2,A3,DIRAF:def 4;
hence thesis by A1,A2,A3,Th12;
end;
theorem
Th22: Mid p,c,b & c,d // b,a & p,d // p,a & not LIN p,a,b & p<>c
implies Mid p,d,a
proof assume that A1: Mid p,c,b and A2: c,d // b,a and
A3: p,d // p,a and A4: not LIN p,a,b and A5: p<>c;
A6: LIN p,c,b by A1,DIRAF:34;
now assume A7: Mid p,a,d; then A8: LIN p,a,d by DIRAF:34;
A9: now assume A10: b<>c & d<>a;
A11: p<>a & p<>b & a<>b by A4,DIRAF:37;
assume not Mid p,d,a; then Mid p,a,d by A3,DIRAF:11;
then p,a // a,d by DIRAF:def 3; then consider e1 such that
A12: c,a // a,e1 and A13: c,p // d,e1 by A11,ANALOAF:def 5;
A14: Mid c,a,e1 by A12,DIRAF:def 3; then A15: LIN c,a,e1 by DIRAF:34;
consider e2 such that
A16: b,a // a,e2 and A17: b,c // e1,e2 by A4,A6,A12,ANALOAF:def 5;
Mid b,a,e2 by A16,DIRAF:def 3; then LIN b,a,e2 by DIRAF:34;
then A18: LIN a,e2,b by DIRAF:36;
A19: b<>e2 by A11,A16,ANALOAF:def 5;
A20: d<>e1
proof assume d=e1; then LIN c,a,d by A14,DIRAF:34;
then LIN a,d,c & (Mid p,d,a or Mid p,a,d) by A3,DIRAF:11,36;
then LIN a,d,c & (LIN p,d,a or LIN p,a,d) by DIRAF:34;
then LIN d,a,c & LIN d,a,p by DIRAF:36;
then LIN d,a,b & LIN d,a,p & LIN d,a,a by A5,A6,DIRAF:37,41;
hence contradiction by A4,A10,DIRAF:38; end;
A21: c <>e1
proof assume c =e1; then Mid c,a,c by A12,DIRAF:def 3;
hence contradiction by A4,A6,DIRAF:12;
end;
consider e3 such that
A22: b,c // e2,e3 and A23: b,e2 // c,e3 & c <>e3 by ANALOAF:def 5;
A24: LIN d,e3,c
proof b,a // b,e2 by A16,ANALOAF:def 5;
then c,d // b,e2 by A2,A11,DIRAF:6;
then c,d // c,e3 by A19,A23,DIRAF:6;
then Mid c,d,e3 or Mid c,e3,d by DIRAF:11;
then LIN c,d,e3 or LIN c,e3,d by DIRAF:34;
hence LIN d,e3,c by DIRAF:36;
end;
Mid b,c,p by A1,DIRAF:13; then A25: b,c // c,p by DIRAF:def 3;
then e1,e2 // c,p by A10,A17,ANALOAF:def 5;
then A26: e1,e2 // d,e1 by A5,A13,DIRAF:6;
then d,e1 // e1,e2 by DIRAF:5;
then A27: d,e1 // d,e2 by ANALOAF:def 5;
then d,e2 // d,e1 & d,e1 // c,p by A13,DIRAF:5;
then d,e2 // c,p & c,p // b,c by A20,A25,DIRAF:5,6;
then d,e2 // b,c by A5,DIRAF:6;
then A28: d,e2 // e2,e3 by A10,A22,DIRAF:6;
then Mid d,e2,e3 by DIRAF:def 3; then A29: LIN d,e2,e3 by DIRAF:34;
A30: d<>e2 by A20,A26,ANALOAF:def 5;
then A31: d<>e3 by A28,ANALOAF:def 5;
A32: a<>e1
proof assume A33: a=e1;
p,a // a,d by A7,DIRAF:def 3;
then d,a // a,p by DIRAF:5;
then c,p // a,p by A10,A13,A33,DIRAF:6;
then p,c // p,a by DIRAF:5;
then Mid p,c,a or Mid p,a,c by DIRAF:11;
then LIN p,c,a or LIN p,a,c by DIRAF:34;
then LIN p,c,a & LIN p,c,p by DIRAF:36,37;
hence contradiction by A4,A5,A6,DIRAF:38;
end;
A34: a<>e2
proof assume A35: a=e2;
e1,a // a,c by A12,DIRAF:5;
then b,c // a,c by A17,A32,A35,DIRAF:6;
then c,b // c,a by DIRAF:5;
then Mid c,b,a or Mid c,a,b by DIRAF:11;
then LIN c,b,a or LIN c,a,b by DIRAF:34;
then LIN c,b,a & LIN c,b,p & LIN c,b,b by A6,DIRAF:36,37;
hence contradiction by A4,A10,DIRAF:38;
end;
d,e2 // d,e3 by A28,ANALOAF:def 5;
then d,e1 // d,e3 by A27,A30,DIRAF:6;
then Mid d,e1,e3 or Mid d,e3,e1 by DIRAF:11;
then LIN d,e1,e3 or LIN d,e3,e1 by DIRAF:34;
then LIN d,e3,e1 & LIN c,e1,a by A15,DIRAF:36;
then A36: LIN d,e3,a by A21,A24,DIRAF:41;
LIN d,e3,e2 by A29,DIRAF:36;
then A37: LIN d,e3,b by A18,A34,A36,DIRAF:41;
LIN c,b,p by A6,DIRAF:36;
then LIN d,e3,p by A10,A24,A37,DIRAF:41;
hence contradiction by A4,A31,A36,A37,DIRAF:38;
end;
now assume b=c;
then Mid b,d,a or Mid b,a,d by A2,DIRAF:11;
then LIN b,d,a or LIN b,a,d by DIRAF:34;
then LIN d,a,b & LIN d,a,p & LIN d,a,a by A8,DIRAF:36,37;
hence a=d by A4,DIRAF:38;
end;
hence thesis by A9,DIRAF:14;
end;
hence thesis by A3,DIRAF:11;
end;
theorem
Th23: Mid p,d,a & c,d // b,a & p,c // p,b & not LIN p,a,b & p<>c
implies Mid p,c,b
proof assume that A1: Mid p,d,a and A2: c,d // b,a and
A3: p,c // p,b and A4: not LIN p,a,b and A5: p<>c;
Mid p,c,b or Mid p,b,c by A3,DIRAF:11;
then A6: LIN p,c,b or LIN p,b,c by DIRAF:34;
then A7: LIN p,c,b by DIRAF:36;
A8: p<>d
proof assume p=d;
then c,p // b,a & c,p // b,p by A2,A3,DIRAF:5;
then b,p // b,a by A5,ANALOAF:def 5;
then Mid b,p,a or Mid b,a,p by DIRAF:11;
then LIN b,p,a or LIN b,a,p by DIRAF:34;
hence contradiction by A4,DIRAF:36;
end;
now assume A9: Mid p,b,c;
p,d // d,a by A1,DIRAF:def 3; then p,d // p,a by ANALOAF:def 5;
then A10: p,a // p,d & b,a // c,d & p<>b by A2,A4,DIRAF:5,37;
not LIN p,d,c
proof assume LIN p,d,c;
then LIN p,c,d & LIN p,c,p by DIRAF:36,37;
then LIN p,d,b & LIN p,d,p & LIN p,d,a by A1,A5,A7,DIRAF:34,38;
hence contradiction by A4,A8,DIRAF:38;
end;
then Mid p,a,d by A9,A10,Th22;
then Mid d,a,p & Mid a,d,p by A1,DIRAF:13;
then c,a // b,a by A2,DIRAF:18; then a,c // a,b by DIRAF:5;
then Mid a,c,b or Mid a,b,c by DIRAF:11;
then LIN a,c,b or LIN a,b,c by DIRAF:34;
then LIN b,c,a & LIN b,c,p & LIN b,c,b by A6,DIRAF:36,37;
then b=c by A4,DIRAF:38;
hence Mid p,c,b by DIRAF:14;
end;
hence thesis by A3,DIRAF:11;
end;
theorem
Th24: not LIN p,a,b & p,b // p,c & b,a // c,d & LIN a,p,d & p<>d
implies not Mid a,p,d
proof assume that A1: not LIN p,a,b and A2: p,b // p,c and
A3: b,a // c,d and LIN a,p,d and A4: p<>d;
A5: a<>p by A1,DIRAF:37;
assume Mid a,p,d; then Mid d,p,a by DIRAF:13;
then A6: d,p // p,a by DIRAF:def 3;
then A7: p,d // a,p by DIRAF:5;
A8: p<>c
proof assume p=c;
then b,a // a,p by A3,A4,A7,DIRAF:6;
then Mid b,a,p by DIRAF:def 3; then Mid p,a,b by DIRAF:13;
hence contradiction by A1,DIRAF:34;
end;
A9: c <>d
proof assume c =d;
then p,b // a,p by A2,A4,A7,DIRAF:6;
then b,p // p,a by DIRAF:5; then Mid b,p,a by DIRAF:def 3;
then LIN b,p,a by DIRAF:34;
hence contradiction by A1,DIRAF:36;
end;
consider b' such that
A10: c,p // p,b' & c,d // a,b' by A4,A6,ANALOAF:def 5;
A11: p<>b'
proof assume p=b';
then b,a // a,p by A3,A9,A10,DIRAF:6;
then Mid b,a,p by DIRAF:def 3; then Mid p,a,b by DIRAF:13;
hence contradiction by A1,DIRAF:34;
end;
p,c // b',p by A10,DIRAF:5; then p,b // b',p by A2,A8,DIRAF:6;
then b',p // p,b by DIRAF:5;
then consider b'' be Element of OAS
such that A12: a,p // p,b'' & a,b' // b,b'' by A11,ANALOAF:def 5;
Mid a,p,b'' by A12,DIRAF:def 3; then LIN a,p,b'' by DIRAF:34;
then A13: LIN a,b'',p by DIRAF:36;
A14: a<>b'' by A5,A12,ANALOAF:def 5;
A15: a<>b'
proof assume a=b';
then c,p // p,a & b,p // c,p by A2,A10,DIRAF:5;
then b,p // p,a by A8,DIRAF:6;
then Mid b,p,a by DIRAF:def 3; then LIN b,p,a by DIRAF:34;
hence contradiction by A1,DIRAF:36;
end;
b,a // a,b' by A3,A9,A10,DIRAF:6;
then b,a // b,b'' by A12,A15,DIRAF:6;
then Mid b,a,b'' or Mid b,b'',a by DIRAF:11;
then LIN b,a,b'' or LIN b,b'',a by DIRAF:34;
then LIN a,b'',b & LIN a,b'', a by DIRAF:36,37;
hence contradiction by A1,A13,A14,DIRAF:38;
end;
theorem
Th25: p,b // p,c & b<>p
implies ex x st p,a // p,x & b,a // c,x
proof assume that A1: p,b // p,c and A2: b<>p;
A3: b,p // c,p by A1,DIRAF:5;
A4: p=c implies p,a // p,c & b,a // c,c by DIRAF:7;
A5: p=a implies p,a // p,a & b,a // c,a by A1,DIRAF:4,5;
now assume A6: p<>c & p<>a;
consider e1 such that A7: Mid a,p,e1 & p<>e1 by DIRAF:17;
Mid e1,p,a by A7,DIRAF:13; then A8: e1,p // p,a by DIRAF:def 3;
a,p // p,e1 by A7,DIRAF:def 3; then consider e2 such that
A9: b,p // p,e2 & b,a // e1,e2 by A6,ANALOAF:def 5;
A10: now assume A11: e1<>e2 & e2<>p;
p,b // e2,p by A9,DIRAF:5;
then e2,p // p,c by A1,A2,ANALOAF:def 5; then consider x
such that A12: e1,p // p,x & e1,e2 // c,x by A11,ANALOAF:def 5;
A13: b,a // c,x by A9,A11,A12,DIRAF:6;
p,a // p,x by A7,A8,A12,ANALOAF:def 5;
hence thesis by A13;
end;
A14: now assume A15: e1=e2 & e2<>p;
then p,e2 // a,p by A8,DIRAF:5;
then b,p // a,p by A9,A15,DIRAF:6;
then p,b // p,a by DIRAF:5;
then A16: p,b // p,a & p,a // p,c by A1,A2,ANALOAF:def 5;
A17: p,b // b,a & p,a // a,c implies p,a // p,c & b,a // c,c by
ANALOAF:def 5;
A18: now assume p,b // b,a & p,c // c,a;
then p,c // p,a by ANALOAF:def 5;
hence p,a // p,c & b,a // c,c by DIRAF:5,7;
end;
A19: now assume p,a // a,b & p,a // a,c;
then a,b // a,c by A6,ANALOAF:def 5;
hence p,a // p,a & b,a // c,a by DIRAF:4,5;
end;
now assume p,a // a,b & p,c // c,a;
then p,c // p,a by ANALOAF:def 5;
hence p,a // p,c & b,a // c,c by DIRAF:5,7;
end;
hence thesis by A16,A17,A18,A19,DIRAF:9;
end;
now assume p=e2;
then b,a // p,a by A7,A8,A9,DIRAF:6;
then A20: a,b // a,p by DIRAF:5;
A21: now assume a,b // b,p;
then a,b // b,p & a,b // a,p by ANALOAF:def 5;
then A22: b,p // a,p or a=b by ANALOAF:def 5;
now assume b,p // a,p;
then a,p // c,p by A2,A3,ANALOAF:def 5;
hence p,a // p,c & b,a // c,c by DIRAF:5,7;
end;
hence thesis by A22,DIRAF:4;
end;
now assume a,p // p,b;
then a,p // p,b & a,p // a,b by ANALOAF:def 5;
then a,b // p,b by A6,ANALOAF:def 5; then b,a // b,p by DIRAF:5;
hence p,a // p,p & b,a // c,p by A2,A3,DIRAF:6,7;
end;
hence thesis by A20,A21,DIRAF:9;
end;
hence thesis by A10,A14;
end;
hence thesis by A4,A5;
end;
theorem
Th26: Mid p,c,b implies ex x st Mid p,x,a & b,a // c,x
proof assume A1: Mid p,c,b; then A2: p,c // c,b by DIRAF:def 3;
A3: p=c implies Mid p,p,a & b,a // c,p by DIRAF:7,14;
A4: now assume p=b;
then p=c by A1,DIRAF:12;
hence Mid p,p,a & b,a // c,p by DIRAF:7,14;
end;
A5: b=c implies Mid p,a,a & b,a // c,a by DIRAF:4,14;
now assume A6: p<>c & p<>b & b<>c;
A7: b,p // c,p
proof Mid b,c,p by A1,DIRAF:13; then b,c // c,p by DIRAF:def 3;
then b,c // c,p & b,c // b,p by ANALOAF:def 5;
hence b,p // c,p by A6,ANALOAF:def 5;
end;
A8: now assume A9: not LIN p,a,b;
then p<>b & p,b // p,c by A1,DIRAF:11,37;
then consider x such that
A10: p,a // p,x and A11: b,a // c,x by Th25;
c,x // b,a & p,x // p,a by A10,A11,DIRAF:5;
then Mid p,x,a by A1,A6,A9,Th22;
hence thesis by A11;
end;
now assume A12: LIN p,a,b;
A13: now assume A14: Mid p,a,b;
A15: Mid p,c,a implies Mid p,c,a & b,a // c,c by DIRAF:7;
now assume Mid p,a,c;
then Mid c,a,p & Mid b,a,p by A14,DIRAF:13;
then c,a // a,p & b,a // a,p by DIRAF:def 3;
then A16: a,p // c,a & a,p // b,a by DIRAF:5;
A17: a=p implies Mid p,p,a & b,a // c,p by A7,DIRAF:14;
b,a // c,a implies Mid p,a,a & b,a // c,a by DIRAF:14;
hence thesis by A16,A17,ANALOAF:def 5;
end;
hence thesis by A1,A14,A15,DIRAF:21;
end;
A18: now assume Mid a,p,b; then Mid b,p,a by DIRAF:13;
then b,p // p,a by DIRAF:def 3; then b,p // b,a by ANALOAF:def 5
;
hence Mid p,p,a & b,a // c,p by A6,A7,ANALOAF:def 5,DIRAF:14;
end;
now assume A19: Mid p,b,a;
then p,c // p,b & p,b // b,a by A2,ANALOAF:def 5,DIRAF:def 3;
then p,c // b,a by A6,DIRAF:6;
then b,a // c,b by A2,A6,ANALOAF:def 5;
hence thesis by A19;
end;
hence thesis by A12,A13,A18,DIRAF:35;
end;
hence thesis by A8;
end;
hence thesis by A3,A4,A5;
end;
theorem
Th27: p<>b & Mid p,b,c implies ex x st Mid p,a,x & b,a // c,x
proof assume that A1: p<>b and A2: Mid p,b,c;
A3: p,b // b,c by A2,DIRAF:def 3; then A4: p,b // p,c by ANALOAF:def 5;
A5: now assume A6: not LIN p,a,b; consider x such that
A7: p,a // p,x & b,a // c,x by A1,A4,Th25;
A8: p<>c by A1,A2,DIRAF:12;
A9: p<>x
proof assume p=x;
then b,a // c,p & p,b // p,c by A2,A7,DIRAF:11;
then b,a // c,p & c,p // b,p by DIRAF:5;
then b,a // b,p by A8,DIRAF:6;
then Mid b,a,p or Mid b,p,a by DIRAF:11;
then LIN b,a,p or LIN b,p,a by DIRAF:34;
hence contradiction by A6,DIRAF:36;
end;
not LIN p,x,c
proof assume A10: LIN p,x,c;
Mid p,a,x or Mid p,x,a by A7,DIRAF:11;
then LIN p,a,x or LIN p,x,a by DIRAF:34;
then LIN p,x,a & LIN p,x,p by DIRAF:36,37;
then LIN p,c,a & LIN p,b,c by A2,A9,A10,DIRAF:34,38;
then LIN p,c,a & LIN p,c,b & LIN p,c,p by DIRAF:36,37;
hence contradiction by A6,A8,DIRAF:38;
end;
then Mid p,a,x by A1,A2,A7,Th22;
hence thesis by A7;
end;
A11: now assume A12: LIN p,a,b & c <>b;
A13: now assume Mid p,a,b; then Mid a,b,c by A2,DIRAF:15;
then Mid c,b,a by DIRAF:13;
then c,b // b,a by DIRAF:def 3;
then c,b // b,a & c,b // c,a by ANALOAF:def 5;
hence Mid p,a,a & b,a // c,a by A12,ANALOAF:def 5,DIRAF:14;
end;
A14: now assume Mid a,p,b; then Mid a,b,c by A1,A2,DIRAF:16;
then Mid c,b,a by DIRAF:13;
then c,b // b,a by DIRAF:def 3;
then c,b // b,a & c,b // c,a by ANALOAF:def 5;
hence Mid p,a,a & b,a // c,a by A12,ANALOAF:def 5,DIRAF:14;
end;
now assume Mid p,b,a; then A15: p,b // b,a by DIRAF:def 3;
then A16: b,a // b,c by A1,A3,ANALOAF:def 5;
A17: now assume A18: b,a // a,c;
p,b // p,a by A15,ANALOAF:def 5;
then A19: b,a // p,a by A1,A15,ANALOAF:def 5;
A20: now assume a=b;
then Mid p,a,a & b,a // c,a
by DIRAF:7,14;
hence thesis;
end;
now assume p,a // a,c;
then Mid p,a,c & b,a // c,c by DIRAF:7,def 3;
hence thesis;
end;
hence thesis by A18,A19,A20,ANALOAF:def 5;
end;
now assume b,c // c,a;
then b,c // c,a & b,c // b,a by ANALOAF:def 5;
hence Mid p,a,a & b,a // c,a by A12,ANALOAF:def 5,DIRAF:14;
end;
hence thesis by A16,A17,ANALOAF:def 5;
end;
hence thesis by A12,A13,A14,DIRAF:35;
end;
c =b implies Mid p,a,a & b,a // c,a by DIRAF:4,14;
hence thesis by A5,A11;
end;
theorem
Th28: not LIN p,a,b & Mid p,c,b
implies ex x st Mid p,x,a & a,b // x,c
proof assume that A1: not LIN p,a,b and A2: Mid p,c,b;
A3: p<>a & p<>b & a<>b by A1,DIRAF:37;
A4: LIN p,c,b by A2,DIRAF:34;
A5: Mid b,c,p by A2,DIRAF:13; then A6: b,c // c,p by DIRAF:def 3;
A7: now assume A8: b<>c & a<>c & p<>c;
consider e1 such that
A9: Mid b,e1,a & p,a // c,e1 by A5,Th26;
consider e2 such that
A10: a,c // c,e2 & a,b // p,e2 by A6,A8,ANALOAF:def 5;
consider e3 such that
A11: p,c // c,e3 & p,a // e2,e3 by A8,A10,ANALOAF:def 5;
consider e4 such that
A12: e1,c // c,e4 & e1,b // p,e4 by A6,A8,ANALOAF:def 5;
consider e5 such that
A13: e4,e2 // c,e5 & e4,c // e2,e5 & e2<>e5 by ANALOAF:def 5;
A14: e3,c // c,p by A11,DIRAF:5;
A15: not LIN p,c,a
proof assume LIN p,c,a;
then LIN p,c,a & LIN p,c,p by DIRAF:37;
hence contradiction by A1,A4,A8,DIRAF:38;
end;
A16: not LIN a,b,c
proof assume LIN a,b,c;
then LIN b,c,a & LIN b,c,p & LIN b,c,b
by A4,DIRAF:36,37;
hence contradiction by A1,A8,DIRAF:38;
end;
A17: p<>e2
proof assume p=e2;
then Mid a,c,p by A10,DIRAF:def 3; then Mid p,c,a by DIRAF:13;
hence contradiction by A15,DIRAF:34;
end;
A18: c <>e2
proof assume A19: c =e2;
p,c // c,b by A6,DIRAF:5;
then a,b // c,b by A8,A10,A19,DIRAF:6;
then b,a // b,c by DIRAF:5;
then Mid b,a,c or Mid b,c,a by DIRAF:11;
then LIN b,a,c or LIN b,c,a by DIRAF:34;
hence contradiction by A16,DIRAF:36;
end;
A20: c <>e3
proof assume c =e3;
then c,e2 // a,p by A11,DIRAF:5;
then a,c // a,p by A10,A18,DIRAF:6;
then Mid a,c,p or Mid a,p,c by DIRAF:11;
then LIN a,c,p or LIN a,p,c by DIRAF:34;
hence contradiction by A15,DIRAF:36;
end;
then consider x such that
A21: e5,c // c,x & e5,e3 // p,x by A14,ANALOAF:def 5;
A22: p<>e3 by A8,A11,ANALOAF:def 5;
A23: not LIN p,e3,e2
proof assume A24: LIN p,e3,e2; p,c // p,e3 by A11,ANALOAF:def 5;
then Mid p,c,e3 or Mid p,e3,c by DIRAF:11;
then LIN p,c,e3 or LIN p,e3,c by DIRAF:34;
then A25: LIN p,e3,c by DIRAF:36;
a,c // a,e2 by A10,ANALOAF:def 5;
then Mid a,c,e2 or Mid a,e2,c by DIRAF:11;
then LIN a,c,e2 or LIN a,e2,c by DIRAF:34;
then LIN c,e2,a by DIRAF:36;
then A26: LIN p,e3,a by A18,A24,A25,DIRAF:41;
p,c // c,b by A2,DIRAF:def 3;
then p,c // p,b & p,c // p,e3 by A11,ANALOAF:def 5;
then p,b // p,e3 by A8,ANALOAF:def 5;
then Mid p,b,e3 or Mid p,e3,b by DIRAF:11;
then LIN p,b,e3 or LIN p,e3,b by DIRAF:34;
then LIN p,e3,b & LIN p,e3,p by DIRAF:36,37;
hence contradiction by A1,A22,A26,DIRAF:38;
end;
A27: c <>e1
proof assume c =e1;
then LIN b,c,a by A9,DIRAF:34;
hence contradiction by A16,DIRAF:36;
end;
A28: e4,c // e2,e3
proof A29: c,e1 // e2,e3 by A3,A9,A11,ANALOAF:def 5;
Mid e1,c,e4 by A12,DIRAF:def 3;
then Mid e4,c,e1 by DIRAF:13;
then e4,c // c,e1 by DIRAF:def 3;
hence e4,c // e2,e3 by A27,A29,DIRAF:6;
end;
A30: b<>e1
proof assume b=e1;
then p,a // c,b & p,c // c,b by A2,A9,DIRAF:def 3;
then p,a // c,b & c,b // p,c by DIRAF:5;
then p,a // p,c by A8,DIRAF:6;
then Mid p,a,c or Mid p,c,a by DIRAF:11;
then LIN p,a,c or LIN p,c,a by DIRAF:34;
hence contradiction by A15,DIRAF:36;
end;
A31: p<>e4
proof assume p=e4;
then c,e1 // p,c by A12,DIRAF:5;
then p,a // p,c by A9,A27,DIRAF:6;
then Mid p,a,c or Mid p,c,a by DIRAF:11;
then LIN p,a,c or LIN p,c,a by DIRAF:34;
hence contradiction by A15,DIRAF:36;
end;
A32: e2<>e4
proof assume e2=e4;
then c,e2 // e1,c by A12,DIRAF:5;
then a,c // e1,c by A10,A18,DIRAF:6;
then c,e1 // c,a by DIRAF:5;
then p,a // c,a by A9,A27,DIRAF:6;
then a,p // a,c by DIRAF:5;
then Mid a,p,c or Mid a,c,p by DIRAF:11;
then LIN a,p,c or LIN a,c,p by DIRAF:34;
hence contradiction by A15,DIRAF:36;
end;
A33: c <>e4
proof assume c =e4;
then e1,b // p,c & p,c // c,b by A2,A12,DIRAF:def 3;
then e1,b // c,b by A8,DIRAF:6;
then b,e1 // b,c by DIRAF:5;
then Mid b,e1,c or Mid b,c,e1 by DIRAF:11;
then LIN b,e1,c or LIN b,c,e1 by DIRAF:34;
then LIN b,e1,c & LIN b,e1,a & LIN
b,e1,b by A9,DIRAF:34,36,37;
hence contradiction by A16,A30,DIRAF:38;
end;
A34: c <>e5
proof assume c =e5; then c,e4 // c,e2 by A13,DIRAF:5;
then e1,c // c,e2 by A12,A33,DIRAF:6;
then c,e2 // e1,c by DIRAF:5;
then a,c // e1,c by A10,A18,DIRAF:6;
then c,e1 // c,a by DIRAF:5;
then p,a // c,a by A9,A27,DIRAF:6;
then a,p // a,c by DIRAF:5;
then Mid a,p,c or Mid a,c,p by DIRAF:11;
then LIN a,p,c or LIN a,c,p by DIRAF:34;
hence contradiction by A15,DIRAF:36;
end;
A35: a<>e1
proof assume a=e1; then a,p // a,c by A9,DIRAF:5;
then Mid a,p,c or Mid a,c,p by DIRAF:11;
then LIN a,p,c or LIN a,c,p by DIRAF:34;
hence contradiction by A15,DIRAF:36;
end;
Mid a,e1,b by A9,DIRAF:13; then a,e1 // e1,b by DIRAF:def 3;
then a,e1 // e1,b & a,e1 // a,b by ANALOAF:def 5;
then a,b // e1,b by A35,ANALOAF:def 5;
then e1,b // p,e2 by A3,A10,ANALOAF:def 5;
then A36: p,e4 // p,e2 by A12,A30,ANALOAF:def 5;
Mid p,c,e3 by A11,DIRAF:def 3;
then Mid p,e4,e2 by A23,A28,A31,A36,Th23;
then p,e4 // e4,e2 by DIRAF:def 3;
then p,e4 // e4,e2 & p,e4 // p,e2 by ANALOAF:def 5;
then A37: p,e2 // e4,e2 by A31,ANALOAF:def 5;
then A38: a,b // e4,e2 by A10,A17,DIRAF:6;
then A39: a,b // c,e5 by A13,A32,DIRAF:6;
a,b // c,e5 & c,e5 // x,c by A13,A21,A32,A38,DIRAF:5,6;
then A40: a,b // x,c by A34,DIRAF:6;
A41: e2<>e3
proof assume e2=e3; then c,e2 // p,c by A11,DIRAF:5;
then a,c // p,c by A10,A18,DIRAF:6;
then c,a // c,p by DIRAF:5;
then Mid c,a,p or Mid c,p,a by DIRAF:11;
then LIN c,a,p or LIN c,p,a by DIRAF:34;
hence contradiction by A15,DIRAF:36;
end;
A42: e5<>e3
proof assume e5=e3; then c,e3 // a,b by A39,DIRAF:5;
then p,c // a,b by A11,A20,DIRAF:6;
then c,p // b,a by DIRAF:5;
then b,c // b,a by A6,A8,DIRAF:6;
then Mid b,c,a or Mid b,a,c by DIRAF:11;
then LIN b,c,a or LIN b,a,c by DIRAF:34;
hence contradiction by A16,DIRAF:36; end;
A43: e3,p // e3,c
proof Mid p,c,e3 by A11,DIRAF:def 3;
then Mid e3,c,p by DIRAF:13;
then e3,c // c,p by DIRAF:def 3;
then e3,c // e3,p by ANALOAF:def 5;
hence e3,p // e3,c by DIRAF:5; end;
A44: p,e2 // c,e5 by A13,A32,A37,DIRAF:6;
A45: LIN e2,e3,e5
proof c,e1 // e4,c by A12,DIRAF:5;
then c,e1 // e2,e5 by A13,A33,DIRAF:6;
then p,a // e2,e5 by A9,A27,DIRAF:6;
then e2,e3 // e2,e5 by A3,A11,ANALOAF:def 5;
then Mid e2,e3,e5 or Mid e2,e5,e3 by DIRAF:11;
then LIN e2,e3,e5 or LIN e2,e5,e3 by DIRAF:34;
hence LIN e2,e3,e5 by DIRAF:36; end;
A46: not LIN e3,e2,p by A23,DIRAF:36;
then not Mid e2,e3,e5 by A42,A43,A44,A45,Th24;
then Mid e3,e2,e5 or Mid e2,e5,e3 by A45,DIRAF:35;
then e3,e2 // e2,e5 or Mid e3,e5,e2 by DIRAF:13,def 3;
then e3,e2 // e3,e5 or e3,e5 // e5,e2 by ANALOAF:def 5,DIRAF:def 3;
then e3,e5 // e3,e2 & c,e5 // p,e2 & Mid p,c,e3
by A11,A44,ANALOAF:def 5,DIRAF:5,def 3;
then e3,e5 // e3,e2 & c,e5 // p,e2 & Mid e3,c,p by DIRAF:13;
then Mid e3,e5,e2 by A20,A46,Th22;
then Mid e2,e5,e3 by DIRAF:13;
then e2,e5 // e5,e3 by DIRAF:def 3;
then e2,e5 // e5,e3 & e2,e5 // e2,e3 by ANALOAF:def 5;
then e2,e3 // e5,e3 by A13,ANALOAF:def 5;
then p,a // e5,e3 by A11,A41,DIRAF:6;
then p,a // p,x by A21,A42,DIRAF:6;
then p,x // p,a & c,x // b,a by A40,DIRAF:5;
then Mid p,x,a by A1,A2,A8,Th22;
hence thesis by A40;
end;
A47: b=c implies a,b // a,c & Mid p,a,a by DIRAF:4,14;
A48: a=c implies a,b // a,c & Mid p,a,a by DIRAF:7,14;
p=c implies a,b // c,c & Mid p,c,a by DIRAF:7,14;
hence thesis by A7,A47,A48;
end;
theorem
ex x st a,x // b,c & a,b // x,c
proof
A1: now assume A2: LIN a,b,c;
A3: Mid a,b,c implies a,b // b,c & a,b // b,c by DIRAF:def 3;
A4: now assume Mid b,a,c; then Mid c,a,b by DIRAF:13;
then c,a // a,b by DIRAF:def 3; then c,a // c,b by ANALOAF:def
5;
hence a,c // b,c & a,b // c,c by DIRAF:5,7;
end;
now assume Mid a,c,b; then a,c // c,b by DIRAF:def 3;
then a,c // a,b by ANALOAF:def 5;
hence a,a // b,c & a,b // a,c by DIRAF:5,7;
end;
hence thesis by A2,A3,A4,DIRAF:35;
end;
now assume A5: not LIN a,b,c;
then A6: a<>b & a<>c & b<>c by DIRAF:37;
consider e1 such that A7: Mid c,a,e1 & a<>e1 by DIRAF:17;
A8: c,a // a,e1 by A7,DIRAF:def 3;
then consider e2 such that
A9: b,a // a,e2 & b,c // e1,e2 by A6,ANALOAF:def 5;
consider e3 such that A10: Mid b,c,e3 & c <>e3 by DIRAF:17;
A11: b,c // c,e3 by A10,DIRAF:def 3;
then consider e4 such that
A12: a,c // c,e4 & a,b // e3,e4 by A6,ANALOAF:def 5;
Mid a,c,e4 by A12,DIRAF:def 3; then A13:Mid e4,c,a by DIRAF:13;
then e4,c // c,a & c,a // c,e1 by A8,ANALOAF:def 5,DIRAF:def 3;
then e4,c // c,e1 by A6,DIRAF:6;
then A14: Mid e4,c,e1 by DIRAF:def 3;
then A15: Mid e1,c,e4 by DIRAF:13;
A16: e4<>c
proof assume e4=c;
then a,b // e3,c & e3,c // c,b by A11,A12,DIRAF:5;
then a,b // c,b by A10,DIRAF:6; then b,a // b,c by DIRAF:5;
then Mid b,a,c or Mid b,c,a by DIRAF:11;
then LIN b,a,c or LIN b,c,a by DIRAF:34;
hence contradiction by A5,DIRAF:36;
end;
then consider e5 such that
A17: Mid e4,e3,e5 & c,e3 // e1,e5 by A14,Th27;
A18: e4<>e3
proof assume e4=e3;
then Mid a,c,e3 by A12,DIRAF:def 3;
then Mid e3,c,a by DIRAF:13;
then LIN e3,c,a & Mid e3,c,b by A10,DIRAF:13,34;
then LIN e3,c,a & LIN e3,c,b & LIN e3,c,c
by DIRAF:34,37;
hence contradiction by A5,A10,DIRAF:38;
end;
then A19: e4<>e5 by A17,DIRAF:12;
A20: e1<>e4 by A14,A16,DIRAF:12;
A21: not LIN e4,c,e3
proof assume LIN e4,c,e3;
then LIN e4,c,e3 & LIN e4,c,a & LIN
e4,c,c by A13,DIRAF:34,37;
then LIN c,e3,a & LIN b,c,e3 by A10,A16,DIRAF:34,38;
then LIN c,e3,a & LIN c,e3,b & LIN c,e3,c
by DIRAF:36,37;
hence contradiction by A5,A10,DIRAF:38;
end;
A22: not LIN e1,e4,e3
proof assume LIN e1,e4,e3;
then LIN e1,e4,e3 & LIN e4,c,e1 by A14,DIRAF:34;
then LIN e4,e1,e3 & LIN e4,e1,c & LIN e4,e1,e4 by DIRAF:36,37;
hence contradiction by A20,A21,DIRAF:38;
end;
A23: not LIN e1,e5,e4
proof assume LIN e1,e5,e4;
then LIN e5,e4,e1 & LIN e4,e3,e5 by A17,DIRAF:34,36;
then LIN e5,e4,e1 & LIN e5,e4,e3 & LIN e5,e4,e4
by DIRAF:36,37;
hence contradiction by A19,A22,DIRAF:38;
end;
then consider e6 such that
A24: Mid e1,e6,e5 & e5,e4 // e6,c by A15,Th28;
consider x such that
A25: Mid c,x,e6 & e1,e6 // a,x by A7,Th26;
A26: e1<>e5 by A23,DIRAF:37;
A27: c <>e1 by A7,DIRAF:12;
A28: not LIN c,e1,b
proof assume LIN c,e1,b;
then LIN c,e1,b & LIN c,a,e1 by A7,DIRAF:34;
then LIN c,e1,b & LIN c,e1,a & LIN c,e1,c by DIRAF:36,37;
hence contradiction by A5,A27,DIRAF:38;
end;
A29: e5<>e3
proof assume e5=e3;
then e3,c // e3,e1 by A17,DIRAF:5;
then Mid e3,c,e1 or Mid e3,e1,c by DIRAF:11;
then LIN e3,c,e1 or LIN e3,e1,c by DIRAF:34;
then LIN e3,c,e1 & Mid e3,c,b by A10,DIRAF:13,36;
then LIN e3,c,e1 & LIN e3,c,b & LIN e3,c,c
by DIRAF:34,37;
hence contradiction by A10,A28,DIRAF:38;
end;
A30: e1<>e6
proof assume A31: e1=e6;
Mid e5,e3,e4 by A17,DIRAF:13; then e5,e3 // e3,e4 by DIRAF:def 3;
then e5,e3 // e3,e4 & e5,e3 // e5,e4 by ANALOAF:def 5;
then e5,e4 // e3,e4 by A29,ANALOAF:def 5;
then e3,e4 // e1,c by A19,A24,A31,ANALOAF:def 5;
then a,b // e1,c & Mid e1,a,c by A7,A12,A18,DIRAF:6,13;
then a,b // e1,c & e1,a // a,c by DIRAF:def 3;
then a,b // e1,c & e1,a // a,c & e1,a // e1,c by ANALOAF:def 5;
then a,b // e1,c & e1,c // a,c by A7,ANALOAF:def 5;
then a,b // a,c by A27,DIRAF:6;
then a,b // b,c or a,c // c,b by DIRAF:9;
then Mid a,b,c or Mid a,c,b by DIRAF:def 3;
then LIN a,b,c or LIN a,c,b by DIRAF:34;
hence contradiction by A5,DIRAF:36;
end;
e1,e6 // e6,e5 by A24,DIRAF:def 3; then e1,e6 // e1,e5 by ANALOAF:def 5
;
then e1,e5 // a,x by A25,A30,ANALOAF:def 5;
then c,e3 // a,x & b,c // c,e3 by A10,A17,A26,DIRAF:6,def 3;
then c,e3 // a,x & c,e3 // b,c by DIRAF:5;
then A32: a,x // b,c by A10,ANALOAF:def 5;
Mid e5,e3,e4 by A17,DIRAF:13; then e5,e3 // e3,e4 by DIRAF:def 3;
then e5,e3 // e3,e4 & e5,e3 // e5,e4 by ANALOAF:def 5;
then e3,e4 // e5,e4 by A29,ANALOAF:def 5;
then a,b // e5,e4 by A12,A18,DIRAF:6;
then A33: a,b // e6,c by A19,A24,DIRAF:6;
A34: e6<>c
proof assume e6=c; then x=c by A25,DIRAF:12;
then c,a // c,b by A32,DIRAF:5;
then Mid c,a,b or Mid c,b,a by DIRAF:11;
then LIN c,a,b or LIN c,b,a by DIRAF:34;
hence contradiction by A5,DIRAF:36;
end;
A35: a<>e2
proof assume a=e2;
then b,c // e1,a & e1,a // a,c by A8,A9,DIRAF:5;
then b,c // a,c by A7,DIRAF:6; then c,b // c,a by DIRAF:5;
then Mid c,b,a or Mid c,a,b by DIRAF:11;
then LIN c,b,a or LIN c,a,b by DIRAF:34;
hence contradiction by A5,DIRAF:36;
end;
A36: e6<>x
proof assume e6=x;
then e6,e1 // e6,a by A25,DIRAF:5;
then Mid e6,e1,a or Mid e6,a,e1 by DIRAF:11;
then LIN e6,e1,a or LIN e6,a,e1 by DIRAF:34;
then LIN e6,e1,a & LIN e1,e6,e5 by A24,DIRAF:34,36;
then LIN e6,e1,a & LIN e6,e1,e5 & LIN e6,e1,e1
by DIRAF:36,37;
then A37: LIN e1,e5,a by A30,DIRAF:38; b,c // e1,e5
by A10,A11,A17,DIRAF:6;
then e1,e2 // e1,e5 by A6,A9,ANALOAF:def 5;
then Mid e1,e2,e5 or Mid e1,e5,e2 by DIRAF:11;
then LIN e1,e2,e5 or LIN e1,e5,e2 by DIRAF:34;
then LIN e1,e5,e2 & LIN e1,e5,e1 by DIRAF:36,37;
then LIN a,e1,e2 & LIN c,a,e1 by A7,A26,A37,DIRAF:34,38;
then LIN a,e1,e2 & LIN a,e1,c & LIN a,e1,a
by DIRAF:36,37;
then LIN a,e2,c & Mid b,a,e2 by A7,A9,DIRAF:38,def 3;
then LIN a,e2,c & LIN b,a,e2 by DIRAF:34;
then LIN a,e2,c & LIN a,e2,b & LIN a,e2,a
by DIRAF:36,37;
hence contradiction by A5,A35,DIRAF:38;
end;
Mid e6,x,c by A25,DIRAF:13;
then e6,x // x,c by DIRAF:def 3;
then e6,x // x,c & e6,x // e6,c by ANALOAF:def 5;
then e6,c // x,c by A36,ANALOAF:def 5;
then a,b // x,c by A33,A34,DIRAF:6;
hence thesis by A32;
end;
hence thesis by A1;
end;
theorem
Th30: a,b // c,d & not LIN a,b,c
implies ex x st Mid a,x,d & Mid b,x,c
proof assume A1: a,b // c,d & not LIN a,b,c;
A2: now assume A3: c =d; take x=c;
thus Mid a,x,d & Mid b,x,c by A3,DIRAF:14;
end;
now assume A4: c <>d;
consider e1 such that
A5: a,b // d,e1 & a,d // b,e1 & b<>e1 by ANALOAF:def 5;
consider e2 such that
A6: c,d // b,e2 & c,b // d,e2 & d<>e2 by ANALOAF:def 5;
A7: a<>b & b<>c by A1,DIRAF:37;
then c,d // d,e1 by A1,A5,ANALOAF:def 5
; then A8: Mid c,d,e1 by DIRAF:def 3;
a,b // b,e2 by A1,A4,A6,DIRAF:6; then A9: Mid a,b,e2 by DIRAF:def 3;
A10: c <>e1
proof assume c =e1;
then c,d // d,c by A1,A5,A7,ANALOAF:def 5;
hence contradiction by A4,ANALOAF:def 5;
end;
A11: a<>e2
proof assume a=e2;
then a,b // b,a by A1,A4,A6,DIRAF:6;
hence contradiction by A7,ANALOAF:def 5;
end;
A12: a<>d
proof assume a=d;
then b,a // a,c by A1,DIRAF:5;
then Mid b,a,c by DIRAF:def 3; then LIN b,a,c by DIRAF:34;
hence contradiction by A1,DIRAF:36;
end;
A13: not LIN c,d,b
proof assume LIN c,d,b; then c,d '||' c,b by DIRAF:def 5;
then A14: c,d // c,b or c,d // b,c by DIRAF:def 4;
now assume c,d // c,b; then a,b // c,b by A1,A4,DIRAF:6;
then b,a // b,c by DIRAF:5;
then Mid b,a,c or Mid b,c,a by DIRAF:11;
then LIN b,a,c or LIN b,c,a by DIRAF:34;
hence contradiction by A1,DIRAF:36;
end;
then a,b // b,c by A1,A4,A14,DIRAF:6;
then Mid a,b,c by DIRAF:def 3;
hence contradiction by A1,DIRAF:34;
end;
A15: not LIN a,b,d
proof assume A16: LIN a,b,d; then A17: a,b '||' a,d by DIRAF:def 5;
A18: now assume a,b // a,d; then c,d // a,d by A1,A7,ANALOAF:def 5;
then d,c // d,a by DIRAF:5; then d,c '||' d,a by DIRAF:def 4;
hence LIN d,c,a by DIRAF:def 5;
end;
now assume a,b // d,a; then c,d // d,a by A1,A7,ANALOAF:def 5;
then Mid c,d,a by DIRAF:def 3; then LIN c,d,a by DIRAF:34;
hence LIN d,c,a by DIRAF:36;
end;
then LIN d,a,a & LIN d,a,c & LIN d,a,b by A16,A17,A18,DIRAF:36,37,def
4;
hence contradiction by A1,A12,DIRAF:38;
end;
A19: not LIN c,b,e1
proof assume LIN c,b,e1;
then LIN c,e1,b & LIN c,d,e1 by A8,DIRAF:34,36;
then LIN c,e1,b & LIN c,e1,d & LIN c,e1,c by DIRAF:36,37;
hence contradiction by A10,A13,DIRAF:38;
end;
A20: not LIN a,d,e2
proof assume LIN a,d,e2;
then LIN a,e2,d & LIN a,b,e2 by A9,DIRAF:34,36;
then LIN a,e2,d & LIN a,e2,b & LIN a,e2,a by DIRAF:36,37;
hence contradiction by A11,A15,DIRAF:38;
end;
consider x such that
A21: Mid c,x,b & b,e1 // x,d by A8,A19,Th28;
consider y such that
A22: Mid a,y,d & d,e2 // y,b by A9,A20,Th28;
c,b // y,b by A6,A22,DIRAF:6; then b,c // b,y by DIRAF:5;
then Mid b,c,y or Mid b,y,c by DIRAF:11;
then LIN b,c,y or LIN b,y,c by DIRAF:34;
then A23: LIN b,c,y by DIRAF:36;
a,d // x,d by A5,A21,DIRAF:6; then d,a // d,x by DIRAF:5;
then Mid d,a,x or Mid d,x,a by DIRAF:11;
then LIN d,a,x or LIN d,x,a by DIRAF:34;
then A24: LIN d,a,x by DIRAF:36;
A25: LIN c,x,b by A21,DIRAF:34;
then A26: LIN b,c,x by DIRAF:36;
LIN b,c,x & LIN b,c,b by A25,DIRAF:36,37;
then A27: LIN x,y,b by A7,A23,DIRAF:38;
LIN a,y,d by A22,DIRAF:34;
then LIN d,a,y & LIN d,a,a by DIRAF:36,37;
then A28: LIN x,y,a by A12,A24,DIRAF:38;
LIN b,c,c by DIRAF:37; then LIN x,y,c by A7,A23,A26,DIRAF:38;
then Mid a,x,d & Mid b,x,c by A1,A21,A22,A27,A28,DIRAF:13,38;
hence thesis;
end;
hence thesis by A2;
end;
canceled;
theorem OAS satisfies_Fano
proof let a,b,c,d;
assume a,b // c,d & a,c // b,d & not LIN a,b,c;
hence thesis by Th30;
end;
theorem
a,b '||' c,d & a,c '||' b,d & not LIN a,b,c
implies ex x st LIN x,a,d & LIN x,b,c
proof assume A1: a,b '||' c,d & a,c '||' b,d & not LIN a,b,c;
then a,b // c,d & a,c // b,d by Th21;
then consider x such that
A2: Mid a,x,d & Mid b,x,c by A1,Th30;
LIN a,x,d & LIN b,x,c by A2,DIRAF:34;
then LIN x,a,d & LIN x,b,c by DIRAF:36;
hence thesis;
end;
theorem
a,b '||' c,d & a,c '||' b,d & not LIN a,b,c & LIN p,a,d &
LIN p,b,c implies not LIN p,a,b
proof assume A1: a,b '||' c,d & a,c '||' b,d & not LIN a,b,c &
LIN p,a,d & LIN p,b,c;
assume A2: LIN p,a,b;
p<>a & LIN p,a,a by A1,DIRAF:37;
then a<>b & LIN a,b,d & a,b '||' d,c by A1,A2,DIRAF:27,38;
hence contradiction by A1,DIRAF:39;
end;
theorem
Th35: Mid a,b,d & Mid b,x,c & not LIN a,b,c
implies ex y st Mid a,y,c & Mid y,x,d
proof assume A1: Mid a,b,d & Mid b,x,c & not LIN a,b,c;
then A2: Mid d,b,a & Mid c,x,b by DIRAF:13;
A3: now assume A4: b<>d & x<>b; d,b // b,a by A2,DIRAF:def 3;
then consider e1 such that
A5: x,b // b,e1 & x,d // a,e1 by A4,ANALOAF:def 5;
A6: Mid x,b,e1 by A5,DIRAF:def 3; then Mid e1,b,x by DIRAF:13;
then A7: Mid e1,x,c by A1,A4,DIRAF:16;
then A8: Mid c,x,e1 by DIRAF:13;
A9: c <>e1
proof assume c =e1;
then Mid x,b,x by A6,A7,DIRAF:12;
hence contradiction by A4,DIRAF:12;
end;
A10: x<>e1 by A4,A6,DIRAF:12;
A11: not LIN c,a,e1
proof assume LIN c,a,e1; then A12: LIN c,e1,a by DIRAF:36;
LIN c,x,e1 by A8,DIRAF:34;
then LIN c,e1,x & LIN x,b,e1 by A6,DIRAF:34,36;
then LIN c,e1,x & LIN c,e1,e1 & LIN x,e1,b by DIRAF:36,37;
then LIN c,e1,b & LIN c,e1,c by A10,DIRAF:37,41;
hence contradiction by A1,A9,A12,DIRAF:38;
end;
then consider y such that
A13: Mid c,y,a & a,e1 // y,x by A8,Th28;
a<>e1 by A11,DIRAF:37; then x,d // y,x by A5,A13,DIRAF:6;
then d,x // x,y by DIRAF:5; then Mid d,x,y by DIRAF:def 3;
then Mid a,y,c & Mid y,x,d by A13,DIRAF:13;
hence thesis;
end;
A14: now assume A15: b<>d & x=b; take y=a;
thus Mid a,y,c & Mid y,x,d by A1,A15,DIRAF:14;
end;
now assume A16: b=d; take y=c;
thus Mid a,y,c & Mid d,x,y by A1,A16,DIRAF:14;
thus Mid a,y,c & Mid y,x,d by A1,A16,DIRAF:13,14;
end;
hence thesis by A3,A14;
end;
theorem OAS satisfies_Ext_Bet_Pasch
proof let a,b,c,d,x,y;
assume Mid a,b,d & Mid b,x,c & not LIN a,b,c;
hence thesis by Th35;
end;
theorem
Th37: Mid a,b,d & Mid a,x,c & not LIN a,b,c
implies ex y st Mid b,y,c & Mid x,y,d
proof assume that A1: Mid a,b,d and
A2: Mid a,x,c and A3: not LIN a,b,c;
A4: a<>b & a<>c & b<>c by A3,DIRAF:37;
A5: now assume A6: b<>d & x<>c & a<>x;
then consider e1 such that
A7: Mid a,d,e1 and A8: x,d // c,e1 by A2,Th27;
A9: Mid d,b,a & Mid e1,d,a by A1,A7,DIRAF:13;
then A10: LIN d,b,a & LIN e1,d,a by DIRAF:34;
A11: e1<>b by A6,A9,DIRAF:18; Mid b,d,e1 by A1,A7,DIRAF:15;
then Mid e1,d,b by DIRAF:13;
then Mid e1,b,a by A9,DIRAF:16;
then e1,b // b,a by DIRAF:def 3; then consider e2 such that
A12: c,b // b,e2 and A13: c,e1 // a,e2 by A11,ANALOAF:def 5;
A14: Mid c,b,e2 by A12,DIRAF:def 3;
then A15: LIN c,b,e2 by DIRAF:34;
A16: a<>d by A1,A6,DIRAF:12;
A17: c <>e1
proof assume c =e1;
then LIN d,a,b & LIN d,a,c & LIN d,a,a
by A10,DIRAF:36,37;
hence contradiction by A3,A16,DIRAF:38;
end;
A18: a<>e2
proof assume a=e2; then Mid c,b,a by A12,DIRAF:def 3;
then Mid a,b,c by DIRAF:13;
hence contradiction by A3,DIRAF:34;
end;
Mid c,x,a by A2,DIRAF:13; then consider y such that
A19: Mid c,y,e2 and A20: a,e2 // x,y by Th26;
A21: not LIN a,x,b
proof assume LIN a,x,b;
then LIN a,x,b & LIN a,x,c & LIN a,x,a
by A2,DIRAF:34,37;
hence contradiction by A3,A6,DIRAF:38;
end;
A22: not LIN x,d,a
proof assume LIN x,d,a;
then LIN d,a,x & LIN d,a,b & LIN d,a,a
by A10,DIRAF:36,37;
hence contradiction by A16,A21,DIRAF:38;
end;
then A23: x<>d by DIRAF:37;
A24: c <>e2 by A4,A12,ANALOAF:def 5;
x,d // a,e2 by A8,A13,A17,DIRAF:6;
then x,d // x,y by A18,A20,DIRAF:6;
then A25: Mid x,d,y or Mid x,y,d by DIRAF:11;
A26: now assume A27: Mid x,d,y; then consider c' such that
A28: Mid x,c',a and A29: Mid c',b,y by A9,A22,Th35;
A30: b<>y
proof assume b=y; then LIN x,d,b by A27,DIRAF:34;
then LIN d,b,x & LIN a,x,c by A2,DIRAF:34,36;
then LIN d,b,c & LIN d,b,b by A6,A10,DIRAF:37,41;
hence contradiction by A3,A6,A10,DIRAF:38;
end;
LIN a,x,c & LIN x,c',a by A2,A28,DIRAF:34;
then LIN x,a,c & LIN x,a,c' & LIN x,a,a
by DIRAF:36,37;
then A31: LIN c,c',a by A6,DIRAF:38;
LIN c,y,e2 & LIN c,b,e2 by A14,A19,DIRAF:34;
then LIN c,e2,y & LIN c,e2,b & LIN c,e2,c
by DIRAF:36,37;
then LIN b,y,c & LIN c',b,y by A24,A29,DIRAF:34,38;
then LIN b,y,c & LIN b,y,c' & LIN b,y,b
by DIRAF:36,37;
then LIN c,c',b & LIN c,c',c by A30,DIRAF:38;
then Mid x,c,a & Mid c,x,a by A2,A3,A28,A31,DIRAF:13,38;
hence contradiction by A6,DIRAF:18;
end;
then A32: Mid d,y,x by A25,DIRAF:13;
A33: Mid c,b,y or Mid c,y,b by A14,A19,DIRAF:21;
now assume A34: not Mid c,y,b;
then A35: y<>b by DIRAF:14;
Mid b,y,e2 by A19,A33,A34,DIRAF:15;
then consider z such that
A36: Mid b,d,z & y,d // e2,z by A35,Th27;
A37: y<>d
proof assume y=d; then LIN c,d,e2 by A19,DIRAF:34;
then A38: LIN c,e2,d & LIN c,e2,b by A15,DIRAF:36;
then LIN c,e2,a & LIN c,e2,c
by A6,A10,DIRAF:37,41;
hence contradiction by A3,A24,A38,DIRAF:38;
end;
d,y // y,x by A32,DIRAF:def 3; then d,y // d,x by ANALOAF:def 5;
then y,d // x,d by DIRAF:5;
then y,d // c,e1 by A8,A23,DIRAF:6;
then c,e1 // e2,z by A36,A37,ANALOAF:def 5;
then a,e2 // e2,z by A13,A17,ANALOAF:def 5;
then Mid a,e2,z by DIRAF:def 3; then LIN a,e2,z by DIRAF:34;
then A39: LIN a,z,e2 by DIRAF:36;
A40: b<>e2
proof assume b=e2;
then c,e1 // a,b & c,e1 // x,d by A8,A13,DIRAF:5;
then a,b // x,d & a,b // b,d by A1,A17,ANALOAF:def 5,DIRAF:def
3;
then x,d // b,d by A4,ANALOAF:def 5;
then d,x // d,b by DIRAF:5;
then Mid d,x,b or Mid d,b,x by DIRAF:11;
then LIN d,x,b or LIN d,b,x by DIRAF:34;
then LIN d,b,x & LIN d,b,b by DIRAF:36,37;
then LIN a,x,b & LIN a,x,c & LIN a,x,a
by A2,A6,A10,DIRAF:34,38;
hence contradiction by A3,A6,DIRAF:38;
end;
LIN b,d,z & LIN b,d,a & LIN b,d,b
by A10,A36,DIRAF:34,36,37;
then A41: LIN a,z,b & LIN a,z,a by A6,DIRAF:38;
now assume a=z;
then Mid b,d,a & Mid d,b,a by A1,A36,DIRAF:13;
hence contradiction by A6,DIRAF:18;
end;
then A42: LIN a,e2,b & LIN a,e2,e2 & LIN b,e2,c
by A15,A39,A41,DIRAF:36,38;
then LIN a,e2,c & LIN a,e2,a by A40,DIRAF:37,41;
hence contradiction by A3,A18,A42,DIRAF:38;
end;
then Mid b,y,c by DIRAF:13;
hence thesis by A25,A26;
end;
A43: b=d implies Mid b,d,c & Mid x,d,d by DIRAF:14;
A44: x=c implies Mid b,c,c & Mid x,c,d by DIRAF:14;
a=x implies Mid b,b,c & Mid x,b,d by A1,DIRAF:14;
hence thesis by A5,A43,A44;
end;
theorem OAS satisfies_Int_Bet_Pasch
proof let a,b,c,d,x,y;
assume Mid a,b,d & Mid a,x,c & not LIN a,b,c;
hence thesis by Th37;
end;
theorem
Mid p,a,b & p,a // p',a' & not LIN p,a,p' & LIN p',a',b' &
p,p' // a,a' & p,p' // b,b' implies Mid p',a',b'
proof assume that A1: Mid p,a,b and A2: p,a // p',a' and
A3: not LIN p,a,p' and A4: LIN p',a',b' and A5: p,p' // a,a'
and A6: p,p' // b,b';
A7: p<>a & p<>p' & a<>p' by A3,DIRAF:37;
A8: LIN p,a,b by A1,DIRAF:34; then A9: LIN p,b,a by DIRAF:36;
now assume A10: p'<>a' & a'<>b';
consider x such that
A11: Mid p,x,b' and A12: b,b' // a,x by A1,Th26;
Mid b',x,p by A11,DIRAF:13;
then consider y such that
A13: Mid b',y,p' and A14: p,p' // x,y by Th26;
A15: LIN b',y,p' & LIN p,x,b' by A11,A13,DIRAF:34;
A16: not LIN p,a,a'
proof assume LIN p,a,a';
then LIN p,a,a' & p,a '||' a',p' by A2,DIRAF:def 4;
hence contradiction by A3,A7,DIRAF:39;
end;
then A17: a<>a' by DIRAF:37;
A18: b<>b'
proof assume b=b'; then LIN a',p',b by A4,DIRAF:36;
then a',p' '||' a',b by DIRAF:def 5;
then a',p' // a',b or a',p' // b,a' by DIRAF:def 4;
then p',a' // a',b or p',a' // b,a' by DIRAF:5;
then p,a // a',b or p,a // b,a' by A2,A10,DIRAF:6;
then p,a '||' b,a' by DIRAF:def 4;
hence contradiction by A7,A8,A16,DIRAF:39;
end;
A19: x<>a
proof assume x=a;
then LIN p,a,b' & LIN p,a,a & LIN p,a,p by A11,DIRAF:34,37;
then A20: LIN b,b',a & LIN b,b',p by A7,A8,DIRAF:38;
b,b' // p,p' by A6,DIRAF:5; then b,b' '||' p,p' by DIRAF:def 4;
then LIN b,b',p' by A18,A20,DIRAF:39;
hence contradiction by A3,A18,A20,DIRAF:38;
end;
A21: p<>b by A1,A7,DIRAF:12;
A22: p'<>b'
proof assume A23: p'=b';
then b',p // b',b by A6,DIRAF:5;
then Mid b',p,b or Mid b',b,p by DIRAF:11;
then LIN b',p,b or LIN b',b,p by DIRAF:34;
then LIN p,b,b' & LIN p,b,b & LIN p,b,p by DIRAF:36,37;
hence contradiction by A3,A9,A21,A23,DIRAF:38;
end;
A24: p,p' // a,x by A6,A12,A18,DIRAF:6;
then a,x // x,y by A7,A14,ANALOAF:def 5;
then a,x // a,y by ANALOAF:def 5; then p,p' // a,y by A19,A24,DIRAF:6;
then a,y // a,a' by A5,A7,ANALOAF:def 5;
then a,y '||' a,a' by DIRAF:def 4;
then LIN a,y,a' by DIRAF:def 5; then A25: LIN y,a',a by DIRAF:36;
LIN p',b',y & LIN p',b',a' & LIN p',b',p'
by A4,A15,DIRAF:36,37;
then LIN y,a',p' & LIN y,a',a' by A22,DIRAF:38;
then A26: y=a' or LIN a,a',p' by A25,DIRAF:38;
now assume LIN a,a',p';
then LIN a,a',p' & a,a' // p,p' by A5,DIRAF:5;
then LIN a,a',p' & a,a' '||' p',p by DIRAF:def 4;
then LIN a,a',p by A17,DIRAF:39;
hence contradiction by A16,DIRAF:36;
end;
hence Mid p',a',b' by A13,A26,DIRAF:13;
end;
hence thesis by DIRAF:14;
end;