:: Classical and Non--classical Pasch Configurations in Ordered Affine Planes
::  by Henryk Oryszczyszyn, Krzysztof Pra\.zmowski and
::     Ma{\l}gorzata Pra\.zmowska
::
:: Received May 16, 1990
:: Copyright (c) 1990-2012 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 ANALOAF, SUBSET_1, DIRAF, PARSP_1, VECTSP_1, PASCH;
 notations STRUCT_0, ANALOAF, DIRAF;
 constructors DIRAF;
 registrations STRUCT_0;
 theorems DIRAF, ANALOAF;

begin

reserve OAS for OAffinSpace;
reserve a,a9,b,b9,c,c9,d,d1,d2,e1,e2,e3,e4,e5,e6,p,p9,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;
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;
end;

definition
  let OAS;
  attr OAS is satisfying_Gen_Par_Pasch means
  for a,b,c,a9,b9,c9 st not LIN a,b
,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 holds Mid a9,
  b9,c9;
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;
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;
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;
end;

theorem Th1:
  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
A5: now
      Mid b,p,c by A1,DIRAF:def 3;
      then LIN b,p,c by DIRAF:28;
      then
A6:   LIN p,c,b by DIRAF:30;
      assume p,a // p,b;
      then
A7:   a,p // b,p by DIRAF:2;
      then a,p // p,c by A1,A3,DIRAF:3;
      then Mid a,p,c by DIRAF:def 3;
      then LIN a,p,c by DIRAF:28;
      then LIN p,c,a by DIRAF:30;
      then
A8:   p,c '||' a,b by A6,DIRAF:34;
A9:   p,c // b,p by A1,DIRAF:2;
A10:  LIN p,c,c by DIRAF:31;
      consider d such that
A11:  Mid p,c,d and
A12:  c <>d by DIRAF:13;
A13:  p<>d by A11,A12,DIRAF:8;
      p,c // c,d by A11,DIRAF:def 3;
      then p,c // p,d by ANALOAF:def 5;
      then
A14:  b,p // p,d by A2,A9,ANALOAF:def 5;
      LIN p,c,d by A11,DIRAF:28;
      then p,c '||' c,d by A10,DIRAF:34;
      then a,b '||' c,d by A2,A8,DIRAF:23;
      hence thesis by A3,A7,A12,A13,A14,DIRAF:3;
    end;
A15: now
      assume p,a // b,p;
      then
A16:  a,p // p,b by DIRAF:2;
      then Mid a,p,b by DIRAF:def 3;
      then LIN a,p,b by DIRAF:28;
      then
A17:  LIN p,b,a by DIRAF:30;
      Mid b,p,c by A1,DIRAF:def 3;
      then LIN b,p,c by DIRAF:28;
      then
A18:  LIN p,b,c by DIRAF:30;
A19:  LIN a,b,b by DIRAF:31;
A20:  b <> c by A1,A2,ANALOAF:def 5;
      LIN p,b,b by DIRAF:31;
      then LIN a,b,c by A3,A17,A18,DIRAF:32;
      hence thesis by A3,A16,A20,A19,DIRAF:34;
    end;
    assume LIN a,b,p;
    then LIN p,a,b by DIRAF:30;
    then p,a '||' p,b by DIRAF:def 5;
    hence thesis by A5,A15,DIRAF:def 4;
  end;
  now
    consider d such that
A21: a,p // p,d and
A22: a,b // c,d by A1,A3,ANALOAF:def 5;
    assume
A23: not LIN a,b,p;
A24: now
      assume d=p;
      then p,c // b,a by A22,DIRAF:2;
      then b,p // b,a by A1,A2,DIRAF:3;
      then b,p '||' b,a by DIRAF:def 4;
      then LIN b,p,a by DIRAF:def 5;
      hence contradiction by A23,DIRAF:30;
    end;
A25: now
      assume d=c;
      then p,d // b,p by A1,DIRAF:2;
      then a,p // b,p by A21,A24,DIRAF:3;
      then p,a // p,b by DIRAF:2;
      then p,a '||' p,b by DIRAF:def 4;
      then LIN p,a,b by DIRAF:def 5;
      hence contradiction by A23,DIRAF:30;
    end;
    a,b '||' c,d by A22,DIRAF:def 4;
    hence thesis by A21,A24,A25;
  end;
  hence thesis by A4;
end;

theorem Th2:
  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:13;
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,Th1;
  b,p // c,p by A1,DIRAF:2;
  then p,q // c,p by A3,A6,ANALOAF:def 5;
  then q,p // p,c by DIRAF:2;
  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,Th1;
  p,r // d,p by A11,DIRAF:2;
  then a,p // d,p by A7,A10,DIRAF:3;
  then
A14: p,a // p,d by DIRAF:2;
  q,r '||' c,d by A12,DIRAF:22;
  then a,b '||' c,d by A8,A9,DIRAF:23;
  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 // c,p;
      then b,p // p,c by DIRAF:2;
      then consider d such that
A6:   a,p // p,d and
A7:   a,b '||' c,d and
      c <>d and
      d<>p by A2,A4,Th1;
      p,a // d,p by A6,DIRAF:2;
      then p,a '||' p,d by DIRAF:def 4;
      hence thesis by A7;
    end;
    now
      assume p,b // p,c;
      then consider d such that
A8:   p,a // p,d and
A9:   a,b '||' c,d and
      c <>d by A2,A4,Th2;
      p,a '||' p,d by A8,DIRAF:def 4;
      hence thesis by A9;
    end;
    hence thesis by A1,A5,DIRAF:def 4;
  end;
  now
A10: a,b '||' p,p by DIRAF:20;
A11: p,a '||' p,p by DIRAF:20;
    assume p=c;
    hence thesis by A11,A10;
  end;
  hence thesis by A3;
end;

theorem Th4:
  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: p<>a by A1,DIRAF:31;
A8: a<>b by A1,DIRAF:31;
A9: now
    LIN p,a,a by DIRAF:31;
    then
A10: LIN d1,d2,a by A3,A4,A7,DIRAF:32;
A11: LIN d1,d2,d1 by DIRAF:31;
A12: LIN p,c,b by A2,DIRAF:30;
A13: LIN d1,d2,d2 by DIRAF:31;
A14: LIN p,a,p by DIRAF:31;
    then
A15: LIN d1,d2,p by A3,A4,A7,DIRAF:32;
    c,d1 '||' c,d2 by A5,A6,A8,DIRAF:23;
    then
A16: LIN c,d1,d2 by DIRAF:def 5;
    then
A17: LIN d1,d2,c by DIRAF:30;
    assume
A18: p<>c;
    assume
A19: d1<>d2;
    LIN d1,d2,p by A3,A4,A7,A14,DIRAF:32;
    then
A20: LIN p,c,d1 by A19,A17,A11,DIRAF:32;
    LIN d1,d2,c by A16,DIRAF:30;
    then LIN p,c,d2 by A19,A15,A13,DIRAF:32;
    then LIN d1,d2,b by A18,A20,A12,DIRAF:32;
    hence contradiction by A1,A19,A15,A10,DIRAF:32;
  end;
A21: LIN p,d2,a by A4,DIRAF:30;
A22: LIN p,d1,a by A3,DIRAF:30;
  now
A23: LIN p,d2,p by DIRAF:31;
    assume
A24: c =p;
    then
A25: p,d2 '||' a,b by A6,DIRAF:22;
A26: now
      assume
A27:  p<>d2;
      then LIN p,d2,b by A21,A25,DIRAF:33;
      hence contradiction by A1,A21,A23,A27,DIRAF:32;
    end;
A28: LIN p,d1,p by DIRAF:31;
A29: p,d1 '||' a,b by A5,A24,DIRAF:22;
    now
      assume
A30:  p<>d1;
      then LIN p,d1,b by A22,A29,DIRAF:33;
      hence contradiction by A1,A22,A28,A30,DIRAF:32;
    end;
    hence thesis by A26;
  end;
  hence thesis by A9;
end;

theorem Th5:
  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;
  a<>c by A1,DIRAF:31;
  then b,d1 '||' b,d2 by A4,A5,DIRAF:23;
  then LIN b,d1,d2 by DIRAF:def 5;
  then
A7: LIN d1,d2,b by DIRAF:30;
A8: now
    assume c =d1;
    then c,a '||' c,b by A4,DIRAF:22;
    then LIN c,a,b by DIRAF:def 5;
    hence contradiction by A1,DIRAF:30;
  end;
A9: LIN d1,d2,d1 by DIRAF:31;
  a<>b by A1,DIRAF:31;
  then c,d1 '||' c,d2 by A2,A3,DIRAF:23;
  then
A10: LIN c,d1,d2 by DIRAF:def 5;
  then
A11: LIN d1,d2,c by DIRAF:30;
  LIN d1,d2,c by A10,DIRAF:30;
  then d1,d2 '||' c,d1 by A9,DIRAF:34;
  then d1,d2 '||' a,b or c =d1 by A2,DIRAF:23;
  then d1,d2 '||' b,a by A8,DIRAF:22;
  then LIN d1,d2,a by A6,A7,DIRAF:33;
  hence contradiction by A1,A6,A11,A7,DIRAF:32;
end;

theorem Th6:
  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;
A5: LIN p,d,c by A3,DIRAF:30;
  LIN b,p,a by A2,DIRAF:28;
  then
A6: LIN p,b,a by DIRAF:30;
  p,c '||' p,d by A3,DIRAF:def 5;
  then
A7: p,c // p,d or p,c // d,p by DIRAF:def 4;
  assume
A8: not Mid c,p,d;
  then
A9: d<>p by DIRAF:10;
A10: now
    assume p,c // d,p;
    then c,p // p,d by DIRAF:2;
    hence contradiction by A8,DIRAF:def 3;
  end;
  p<>c by A8,DIRAF:10;
  then consider q such that
A11: p,b // p,q and
A12: b,c '||' d,q and
  d<>q by A9,A7,A10,Th2;
A13: LIN p,d,p by DIRAF:31;
  p,b '||' p,q by A11,DIRAF:def 4;
  then LIN p,b,q by DIRAF:def 5;
  then a=q by A1,A3,A4,A12,A6,Th4;
  then b,p // p,q by A2,DIRAF:def 3;
  then p,q // b,p by DIRAF:2;
  then p,b // b,p or p=q by A11,DIRAF:3;
  then p=b or p=q by ANALOAF:def 5;
  then p,d '||' c,b by A1,A12,DIRAF:22,31;
  then LIN p,d,b by A9,A5,DIRAF:33;
  hence contradiction by A1,A9,A5,A13,DIRAF:32;
end;

theorem
  OAS is satisfying_Int_Par_Pasch
proof
  let a,b,c,d,p;
  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;
  thus thesis by A1,A2,A3,A4,Th6;
end;

theorem Th8:
  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
    LIN d,a,p by A2,DIRAF:30;
    then d,a '||' d,p by DIRAF:def 5;
    then
A6: a,d '||' d,p by DIRAF:22;
    assume
A7: b<>c;
A8: b<>a by A4,DIRAF:31;
A9: not LIN d,b,a
    proof
      assume LIN d,b,a;
      then
A10:  LIN a,b,d by DIRAF:30;
      a,b '||' d,c by A3,DIRAF:22;
      then LIN a,b,c by A8,A10,DIRAF:33;
      then
A11:  LIN b,c,a by DIRAF:30;
      LIN p,b,c by A1,DIRAF:28;
      then
A12:  LIN b,c,p by DIRAF:30;
      LIN b,c,b by DIRAF:31;
      hence contradiction by A4,A7,A11,A12,DIRAF:32;
    end;
    then d<>a by DIRAF:31;
    then consider q such that
A13: b,d '||' d,q and
A14: b,a '||' p,q by A6,DIRAF:27;
A15: LIN p,b,c by A1,DIRAF:28;
A16: p<>c by A1,A7,DIRAF:8;
A17: not LIN b,c,d
    proof
A18:  LIN p,c,c by DIRAF:31;
      LIN p,b,c by A1,DIRAF:28;
      then
A19:  LIN p,c,b by DIRAF:30;
      assume
A20:  LIN b,c,d;
A21:  LIN b,c,b by DIRAF:31;
A22:  now
        assume a,b '||' c,b;
        then b,c '||' b,a by DIRAF:22;
        then LIN b,c,a by DIRAF:def 5;
        hence contradiction by A7,A9,A20,A21,DIRAF:32;
      end;
      LIN c,d,b by A20,DIRAF:30;
      then c,d '||' c,b by DIRAF:def 5;
      then LIN p,a,c by A2,A3,A22,DIRAF:23;
      then LIN p,c,a by DIRAF:30;
      then LIN b,c,a by A16,A19,A18,DIRAF:32;
      hence contradiction by A7,A9,A20,A21,DIRAF:32;
    end;
    a,b '||' q,p by A14,DIRAF:22;
    then
A23: c,d '||' q,p by A3,A8,DIRAF:23;
    d,b '||' d,q by A13,DIRAF:22;
    then LIN d,b,q by DIRAF:def 5;
    then
A24: LIN b,d,q by DIRAF:30;
A25: d<>p
    proof
A26:  LIN p,c,p by DIRAF:31;
      LIN p,b,c by A1,DIRAF:28;
      then
A27:  LIN p,c,b by DIRAF:30;
      assume d=p;
      then p,c '||' b,a by A3,DIRAF:22;
      then LIN p,c,a by A16,A27,DIRAF:33;
      hence contradiction by A4,A16,A27,A26,DIRAF:32;
    end;
A28: not LIN d,p,q
    proof
A29:  now
        assume p=q;
        then d,b '||' d,p by A13,DIRAF:22;
        then LIN d,b,p by DIRAF:def 5;
        then
A30:    LIN d,p,b by DIRAF:30;
A31:    LIN d,p,d by DIRAF:31;
        LIN d,p,a by A2,DIRAF:30;
        hence contradiction by A9,A25,A31,A30,DIRAF:32;
      end;
A32:  LIN p,q,p by DIRAF:31;
A33:  LIN d,p,p by DIRAF:31;
      assume
A34:  LIN d,p,q;
      LIN d,p,a by A2,DIRAF:30;
      then
A35:  LIN p,q,a by A25,A34,A33,DIRAF:32;
      p,q '||' a,b by A14,DIRAF:22;
      then LIN p,q,b by A35,A29,DIRAF:33;
      hence contradiction by A4,A35,A29,A32,DIRAF:32;
    end;
    Mid c,b,p by A1,DIRAF:9;
    then
A36: Mid d,b,q by A17,A24,A23,Th6;
A37: now
      d,b '||' d,q by A13,DIRAF:22;
      then LIN d,b,q by DIRAF:def 5;
      then
A38:  LIN d,q,b by DIRAF:30;
      assume
A39:  Mid p,d,a;
      p,q '||' b,a by A14,DIRAF:22;
      then Mid q,d,b by A28,A39,A38,Th6;
      then Mid b,d,q by DIRAF:9;
      then b=d by A36,DIRAF:14;
      hence contradiction by A9,DIRAF:31;
    end;
    assume not Mid p,a,d;
    then Mid a,p,d by A2,A37,DIRAF:29;
    then Mid b,p,c by A3,A4,A15,Th6;
    then p=b by A1,DIRAF:14;
    hence contradiction by A4,DIRAF:31;
  end;
  now
A40: a,b '||' b,a by DIRAF:19;
A41: LIN p,a,a by DIRAF:31;
A42: LIN p,b,b by DIRAF:31;
    assume b=c;
    then a=d by A2,A3,A4,A42,A41,A40,Th4;
    hence thesis by DIRAF:10;
  end;
  hence thesis by A5;
end;

theorem
  OAS is satisfying_Ext_Par_Pasch
proof
  let a,b,c,d,p;
  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;
  thus thesis by A1,A2,A3,A4,Th8;
end;

theorem Th10:
  not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c &
  LIN a9,b9,c9 implies Mid a9,b9,c9
proof
  assume that
A1: not LIN a,b,a9 and
A2: a,a9 '||' b,b9 and
A3: a,a9 '||' c,c9 and
A4: Mid a,b,c and
A5: LIN a9,b9,c9;
A6: LIN a,b,c by A4,DIRAF:28;
A7: LIN b9,c9,a9 by A5,DIRAF:30;
A8: LIN c9,b9,a9 by A5,DIRAF:30;
A9: a<>a9 by A1,DIRAF:31;
  then
A10: b,b9 '||' c,c9 by A2,A3,DIRAF:23;
A11: a<>b by A1,DIRAF:31;
  then
A12: a<>c by A4,DIRAF:8;
A13: now
    assume that
A14: b9<>c9 and
    a9<>b9 and
A15: b<>b9;
A16: not LIN b,b9,a9
    proof
A17:  LIN b,b9,b by DIRAF:31;
      assume
A18:  LIN b,b9,a9;
      b,b9 '||' a9,a by A2,DIRAF:22;
      then LIN b,b9,a by A15,A18,DIRAF:33;
      hence contradiction by A1,A15,A18,A17,DIRAF:32;
    end;
A19: now
      a,b '||' a,c by A6,DIRAF:def 5;
      then c,a '||' a,b by DIRAF:22;
      then consider x such that
A20:  c9,a '||' a,x and
A21:  c9,c '||' b,x by A12,DIRAF:27;
      a,c9 '||' a,x by A20,DIRAF:22;
      then
A22:  LIN a,c9,x by DIRAF:def 5;
      assume
A23:  c <>c9;
A24:  x<>b
      proof
        assume x=b;
        then
A25:    LIN a,b,c9 by A22,DIRAF:30;
        LIN a,b,b by DIRAF:31;
        then
A26:    LIN c,c9,b by A11,A6,A25,DIRAF:32;
        LIN a,b,a by DIRAF:31;
        then LIN c,c9,a by A11,A6,A25,DIRAF:32;
        then c,c9 '||' a,b by A26,DIRAF:34;
        then b,b9 '||' a,b by A10,A23,DIRAF:23;
        then a,a9 '||' a,b by A2,A15,DIRAF:23;
        then LIN a,a9,b by DIRAF:def 5;
        hence contradiction by A1,DIRAF:30;
      end;
      c,c9 '||' b,x by A21,DIRAF:22;
      then b,b9 '||' b,x by A10,A23,DIRAF:23;
      then
A27:  LIN b,b9,x by DIRAF:def 5;
      then LIN b,x,b9 by DIRAF:30;
      then b,x '||' b,b9 by DIRAF:def 5;
      then b,x '||' c,c9 by A10,A15,DIRAF:23;
      then
A28:  x,b '||' c,c9 by DIRAF:22;
A29:  x<>b9
      proof
        assume x=b9;
        then
A30:    LIN b9,c9,a by A22,DIRAF:30;
A31:    a,a9 '||' b9,b by A2,DIRAF:22;
        LIN b9,c9,b9 by DIRAF:31;
        then LIN a,a9,b9 by A7,A14,A30,DIRAF:32;
        then LIN a,a9,b by A9,A31,DIRAF:33;
        hence contradiction by A1,DIRAF:30;
      end;
A32:  not LIN c9,b9,x
      proof
        assume LIN c9,b9,x;
        then
A33:    LIN b9,x,c9 by DIRAF:30;
A34:    LIN b9,x,b9 by DIRAF:31;
A35:    LIN c9,b9,b9 by DIRAF:31;
        LIN b9,x,b by A27,DIRAF:30;
        then LIN c9,b9,b by A29,A33,A34,DIRAF:32;
        hence contradiction by A8,A14,A16,A35,DIRAF:32;
      end;
A36:  LIN x,b,b9 by A27,DIRAF:30;
A37:  not LIN a,x,b
      proof
        assume LIN a,x,b;
        then
A38:    LIN x,b,a by DIRAF:30;
A39:    b,b9 '||' a,a9 by A2,DIRAF:22;
        LIN x,b,b by DIRAF:31;
        then LIN b,b9,a by A36,A24,A38,DIRAF:32;
        hence contradiction by A15,A16,A39,DIRAF:33;
      end;
      LIN b9,b,x by A27,DIRAF:30;
      then b9,b '||' b9,x by DIRAF:def 5;
      then b,b9 '||' b9,x by DIRAF:22;
      then
A40:  b9,x '||' a,a9 by A2,A15,DIRAF:23;
      LIN a,x,c9 by A22,DIRAF:30;
      then Mid a,x,c9 by A4,A28,A37,Th8;
      then Mid c9,x,a by DIRAF:9;
      then Mid c9,b9,a9 by A8,A40,A32,Th8;
      hence thesis by DIRAF:9;
    end;
    c =c9 implies thesis
    proof
A41:  not LIN c9,b9,b
      proof
A42:    LIN c9,b9,b9 by DIRAF:31;
        assume LIN c9,b9,b;
        hence contradiction by A8,A14,A16,A42,DIRAF:32;
      end;
      assume c =c9;
      then
A43:  Mid c9,b,a by A4,DIRAF:9;
      b9,b '||' a,a9 by A2,DIRAF:22;
      then Mid c9,b9,a9 by A8,A43,A41,Th8;
      hence thesis by DIRAF:9;
    end;
    hence thesis by A19;
  end;
  b=b9 implies thesis
  proof
A44: a,a9 '||' c9,c by A3,DIRAF:22;
A45: LIN b9,a9,c9 by A5,DIRAF:30;
    assume
A46: b=b9;
    then not LIN b9,a,a9 by A1,DIRAF:30;
    hence thesis by A4,A46,A45,A44,Th6;
  end;
  hence thesis by A13,DIRAF:10;
end;

theorem
  OAS is satisfying_Gen_Par_Pasch
proof
  let a,b,c,a9,b9,c9;
  assume that
A1: not LIN a,b,a9 and
A2: a,a9 '||' b,b9 and
A3: a,a9 '||' c,c9 and
A4: Mid a,b,c and
A5: LIN a9,b9,c9;
  thus thesis by A1,A2,A3,A4,A5,Th10;
end;

theorem
  not LIN p,a,b & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 implies a,b
  // b9,a9
proof
  assume that
A1: not LIN p,a,b and
A2: a,p // p,a9 and
A3: b,p // p,b9 and
A4: a,b '||' a9,b9;
A5: not LIN p,b,a by A1,DIRAF:30;
  Mid b,p,b9 by A3,DIRAF:def 3;
  then LIN b,p,b9 by DIRAF:28;
  then
A6: LIN p,b,b9 by DIRAF:30;
  Mid a,p,a9 by A2,DIRAF:def 3;
  then LIN a,p,a9 by DIRAF:28;
  then
A7: LIN p,a,a9 by DIRAF:30;
A8: b,a '||' a9,b9 by A4,DIRAF:22;
  a<>p by A1,DIRAF:31;
  then consider q such that
A9: b,p // p,q and
A10: b,a // a9,q by A2,ANALOAF:def 5;
  Mid b,p,q by A9,DIRAF:def 3;
  then LIN b,p,q by DIRAF:28;
  then
A11: LIN p,b,q by DIRAF:30;
  b,a '||' a9,q by A10,DIRAF:def 4;
  then b,a // a9,b9 by A10,A5,A7,A6,A11,A8,Th4;
  hence thesis by DIRAF:2;
end;

theorem
  not LIN p,a,a9 & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 implies a,
  a9 // b,b9
proof
  assume that
A1: not LIN p,a,a9 and
A2: p,a // p,b and
A3: p,a9 // p,b9 and
A4: a,a9 '||' b,b9;
  consider c such that
A5: Mid a,p,c and
A6: p<>c by DIRAF:13;
A7: a,p // p,c by A5,DIRAF:def 3;
A8: a<>p by A1,DIRAF:31;
  then consider c9 such that
A9: a9,p // p,c9 and
A10: a9,a // c,c9 by A7,ANALOAF:def 5;
A11: a9,a '||' c9,c by A10,DIRAF:def 4;
A12: c <>c9
  proof
    assume c =c9;
    then Mid a9,p,c by A9,DIRAF:def 3;
    then LIN a9,p,c by DIRAF:28;
    then
A13: LIN p,c,a9 by DIRAF:30;
    LIN a,p,c by A5,DIRAF:28;
    then
A14: LIN p,c,a by DIRAF:30;
    LIN p,c,p by DIRAF:31;
    hence contradiction by A1,A6,A14,A13,DIRAF:32;
  end;
  p,a // c,p by A7,DIRAF:2;
  then c,p // p,b by A2,A8,ANALOAF:def 5;
  then consider b99 be Element of OAS such that
A15: c9,p // p,b99 and
A16: c9,c // b,b99 by A6,ANALOAF:def 5;
A17: a9,a '||' b,b9 by A4,DIRAF:22;
A18: p<>c9
  proof
    assume p=c9;
    then a9,a '||' c,p by A10,DIRAF:def 4;
    then
A19: p,c '||' a,a9 by DIRAF:22;
    a,p '||' p,c by A7,DIRAF:def 4;
    then a,p '||' a,a9 by A6,A19,DIRAF:23;
    then LIN a,p,a9 by DIRAF:def 5;
    hence contradiction by A1,DIRAF:30;
  end;
  p,a '||' p,b by A2,DIRAF:def 4;
  then
A20: LIN p,a,b by DIRAF:def 5;
A21: c9,c // a,a9 by A10,DIRAF:2;
  a9,p '||' p,c9 by A9,DIRAF:def 4;
  then
A22: p,a9 '||' p,c9 by DIRAF:22;
  p,a9 '||' p,b9 by A3,DIRAF:def 4;
  then
A23: LIN p,a9,b9 by DIRAF:def 5;
  c9,p '||' p,b99 by A15,DIRAF:def 4;
  then p,c9 '||' p,b99 by DIRAF:22;
  then p,a9 '||' p,b99 by A18,A22,DIRAF:23;
  then
A24: LIN p,a9,b99 by DIRAF:def 5;
  c9,c '||' b,b99 by A16,DIRAF:def 4;
  then
A25: a9,a '||' b,b99 by A12,A11,DIRAF:23;
  not LIN p,a9,a by A1,DIRAF:30;
  then c9,c // b,b9 by A20,A23,A17,A16,A24,A25,Th4;
  hence thesis by A12,A21,ANALOAF:def 5;
end;

theorem Th14:
  not LIN p,a,b & p,a '||' b,c & p,b '||' a,c implies p,a // b,c & p,b // a,c
proof
  assume that
A1: not LIN p,a,b and
A2: p,a '||' b,c and
A3: p,b '||' a,c;
  consider d such that
A4: p,a // b,d and
A5: p,b // a,d and
  a<>d by ANALOAF:def 5;
A6: p,b '||' a,d by A5,DIRAF:def 4;
  p,a '||' b,d by A4,DIRAF:def 4;
  hence thesis by A1,A2,A3,A4,A5,A6,Th5;
end;

theorem Th15:
  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:28;
  now
    assume
A7: Mid p,a,d;
A8: now
A9:   p<>a by A4,DIRAF:31;
      assume that
A10:  b<>c and
A11:  d<>a;
      assume not Mid p,d,a;
      then Mid p,a,d by A3,DIRAF:7;
      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 A9,ANALOAF:def 5;
A14:  d,e1 // c,p by A13,DIRAF:2;
A15:  c <>e1
      proof
        assume c =e1;
        then Mid c,a,c by A12,DIRAF:def 3;
        hence contradiction by A4,A6,DIRAF:8;
      end;
      Mid b,c,p by A1,DIRAF:9;
      then
A16:  b,c // c,p by DIRAF:def 3;
      then
A17:  c,p // b,c by DIRAF:2;
      consider e2 such that
A18:  b,a // a,e2 and
A19:  b,c // e1,e2 by A4,A6,A12,ANALOAF:def 5;
      consider e3 such that
A20:  b,c // e2,e3 and
A21:  b,e2 // c,e3 and
      c <>e3 by ANALOAF:def 5;
A22:  a<>b by A4,DIRAF:31;
A23:  Mid c,a,e1 by A12,DIRAF:def 3;
A24:  d<>e1
      proof
        Mid p,d,a or Mid p,a,d by A3,DIRAF:7;
        then LIN p,d,a or LIN p,a,d by DIRAF:28;
        then
A25:    LIN d,a,p by DIRAF:30;
A26:    LIN d,a,a by DIRAF:31;
        assume d=e1;
        then LIN c,a,d by A23,DIRAF:28;
        then LIN d,a,c by DIRAF:30;
        then LIN d,a,b by A5,A6,A25,DIRAF:35;
        hence contradiction by A4,A11,A25,A26,DIRAF:32;
      end;
      b,a // b,e2 by A18,ANALOAF:def 5;
      then
A27:  c,d // b,e2 by A2,A22,DIRAF:3;
      b<>e2 by A22,A18,ANALOAF:def 5;
      then c,d // c,e3 by A21,A27,DIRAF:3;
      then Mid c,d,e3 or Mid c,e3,d by DIRAF:7;
      then LIN c,d,e3 or LIN c,e3,d by DIRAF:28;
      then
A28:  LIN d,e3,c by DIRAF:30;
      e1,e2 // c,p by A10,A19,A16,ANALOAF:def 5;
      then
A29:  e1,e2 // d,e1 by A5,A13,DIRAF:3;
      then d,e1 // e1,e2 by DIRAF:2;
      then
A30:  d,e1 // d,e2 by ANALOAF:def 5;
      then d,e2 // d,e1 by DIRAF:2;
      then d,e2 // c,p by A24,A14,DIRAF:3;
      then d,e2 // b,c by A5,A17,DIRAF:3;
      then
A31:  d,e2 // e2,e3 by A10,A20,DIRAF:3;
      then Mid d,e2,e3 by DIRAF:def 3;
      then LIN d,e2,e3 by DIRAF:28;
      then
A32:  LIN d,e3,e2 by DIRAF:30;
A33:  d<>e2 by A24,A29,ANALOAF:def 5;
      then
A34:  d<>e3 by A31,ANALOAF:def 5;
      d,e2 // d,e3 by A31,ANALOAF:def 5;
      then d,e1 // d,e3 by A30,A33,DIRAF:3;
      then Mid d,e1,e3 or Mid d,e3,e1 by DIRAF:7;
      then LIN d,e1,e3 or LIN d,e3,e1 by DIRAF:28;
      then
A35:  LIN d,e3,e1 by DIRAF:30;
      LIN c,a,e1 by A23,DIRAF:28;
      then LIN c,e1,a by DIRAF:30;
      then
A36:  LIN d,e3,a by A15,A28,A35,DIRAF:35;
A37:  a<>e1
      proof
        p,a // a,d by A7,DIRAF:def 3;
        then
A38:    d,a // a,p by DIRAF:2;
        assume a=e1;
        then c,p // a,p by A11,A13,A38,DIRAF:3;
        then p,c // p,a by DIRAF:2;
        then Mid p,c,a or Mid p,a,c by DIRAF:7;
        then LIN p,c,a or LIN p,a,c by DIRAF:28;
        then
A39:    LIN p,c,a by DIRAF:30;
        LIN p,c,p by DIRAF:31;
        hence contradiction by A4,A5,A6,A39,DIRAF:32;
      end;
A40:  a<>e2
      proof
        assume
A41:    a=e2;
        e1,a // a,c by A12,DIRAF:2;
        then b,c // a,c by A19,A37,A41,DIRAF:3;
        then c,b // c,a by DIRAF:2;
        then Mid c,b,a or Mid c,a,b by DIRAF:7;
        then LIN c,b,a or LIN c,a,b by DIRAF:28;
        then
A42:    LIN c,b,a by DIRAF:30;
A43:    LIN c,b,b by DIRAF:31;
        LIN c,b,p by A6,DIRAF:30;
        hence contradiction by A4,A10,A42,A43,DIRAF:32;
      end;
      Mid b,a,e2 by A18,DIRAF:def 3;
      then LIN b,a,e2 by DIRAF:28;
      then LIN a,e2,b by DIRAF:30;
      then
A44:  LIN d,e3,b by A40,A36,A32,DIRAF:35;
      LIN c,b,p by A6,DIRAF:30;
      then LIN d,e3,p by A10,A28,A44,DIRAF:35;
      hence contradiction by A4,A34,A36,A44,DIRAF:32;
    end;
A45: LIN p,a,d by A7,DIRAF:28;
    now
      assume b=c;
      then Mid b,d,a or Mid b,a,d by A2,DIRAF:7;
      then LIN b,d,a or LIN b,a,d by DIRAF:28;
      then
A46:  LIN d,a,b by DIRAF:30;
A47:  LIN d,a,a by DIRAF:31;
      LIN d,a,p by A45,DIRAF:30;
      hence a=d by A4,A46,A47,DIRAF:32;
    end;
    hence thesis by A8,DIRAF:10;
  end;
  hence thesis by A3,DIRAF:7;
end;

theorem Th16:
  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;
A6: p<>d
  proof
    assume
A7: p=d;
    c,p // b,p by A3,DIRAF:2;
    then b,p // b,a by A2,A5,A7,ANALOAF:def 5;
    then Mid b,p,a or Mid b,a,p by DIRAF:7;
    then LIN b,p,a or LIN b,a,p by DIRAF:28;
    hence contradiction by A4,DIRAF:30;
  end;
  Mid p,c,b or Mid p,b,c by A3,DIRAF:7;
  then
A8: LIN p,c,b or LIN p,b,c by DIRAF:28;
  then
A9: LIN p,c,b by DIRAF:30;
  now
A10: not LIN p,d,c
    proof
      assume LIN p,d,c;
      then
A11:  LIN p,c,d by DIRAF:30;
      LIN p,c,p by DIRAF:31;
      then
A12:  LIN p,d,b by A5,A9,A11,DIRAF:32;
A13:  LIN p,d,p by DIRAF:31;
      LIN p,d,a by A1,DIRAF:28;
      hence contradiction by A4,A6,A12,A13,DIRAF:32;
    end;
    assume
A14: Mid p,b,c;
    p,d // d,a by A1,DIRAF:def 3;
    then p,d // p,a by ANALOAF:def 5;
    then
A15: p,a // p,d by DIRAF:2;
A16: p<>b by A4,DIRAF:31;
    b,a // c,d by A2,DIRAF:2;
    then Mid p,a,d by A14,A15,A16,A10,Th15;
    then
A17: Mid d,a,p by DIRAF:9;
    Mid a,d,p by A1,DIRAF:9;
    then c,a // b,a by A2,A17,DIRAF:14;
    then a,c // a,b by DIRAF:2;
    then Mid a,c,b or Mid a,b,c by DIRAF:7;
    then LIN a,c,b or LIN a,b,c by DIRAF:28;
    then
A18: LIN b,c,a by DIRAF:30;
A19: LIN b,c,b by DIRAF:31;
    LIN b,c,p by A8,DIRAF:30;
    then b=c by A4,A18,A19,DIRAF:32;
    hence thesis by DIRAF:10;
  end;
  hence thesis by A3,DIRAF:7;
end;

theorem Th17:
  not LIN p,a,b & p,b // p,c & b,a // c,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
A4: p<>d;
  assume Mid a,p,d;
  then Mid d,p,a by DIRAF:9;
  then
A5: d,p // p,a by DIRAF:def 3;
  then
A6: p,d // a,p by DIRAF:2;
  consider b9 such that
A7: c,p // p,b9 and
A8: c,d // a,b9 by A4,A5,ANALOAF:def 5;
A9: p<>c
  proof
    assume p=c;
    then b,a // a,p by A3,A4,A6,DIRAF:3;
    then Mid b,a,p by DIRAF:def 3;
    hence contradiction by A1,DIRAF:9,28;
  end;
A10: a<>b9
  proof
    assume
A11: a=b9;
    b,p // c,p by A2,DIRAF:2;
    then b,p // p,a by A9,A7,A11,DIRAF:3;
    then Mid b,p,a by DIRAF:def 3;
    then LIN b,p,a by DIRAF:28;
    hence contradiction by A1,DIRAF:30;
  end;
  p,c // b9,p by A7,DIRAF:2;
  then p,b // b9,p by A2,A9,DIRAF:3;
  then
A12: b9,p // p,b by DIRAF:2;
A13: c <>d
  proof
    assume c =d;
    then p,b // a,p by A2,A4,A6,DIRAF:3;
    then b,p // p,a by DIRAF:2;
    then Mid b,p,a by DIRAF:def 3;
    then LIN b,p,a by DIRAF:28;
    hence contradiction by A1,DIRAF:30;
  end;
  p<>b9
  proof
    assume p=b9;
    then b,a // a,p by A3,A13,A8,DIRAF:3;
    then Mid b,a,p by DIRAF:def 3;
    hence contradiction by A1,DIRAF:9,28;
  end;
  then consider b99 be Element of OAS such that
A14: a,p // p,b99 and
A15: a,b9 // b,b99 by A12,ANALOAF:def 5;
  a<>p by A1,DIRAF:31;
  then
A16: a<>b99 by A14,ANALOAF:def 5;
  b,a // a,b9 by A3,A13,A8,DIRAF:3;
  then b,a // b,b99 by A15,A10,DIRAF:3;
  then Mid b,a,b99 or Mid b,b99,a by DIRAF:7;
  then LIN b,a,b99 or LIN b,b99,a by DIRAF:28;
  then
A17: LIN a,b99,b by DIRAF:30;
  Mid a,p,b99 by A14,DIRAF:def 3;
  then LIN a,p,b99 by DIRAF:28;
  then
A18: LIN a,b99,p by DIRAF:30;
  LIN a,b99, a by DIRAF:31;
  hence contradiction by A1,A18,A16,A17,DIRAF:32;
end;

theorem Th18:
  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:2;
A4: now
    assume that
    p<>c and
A5: p<>a;
    consider e1 such that
A6: Mid a,p,e1 and
A7: p<>e1 by DIRAF:13;
    a,p // p,e1 by A6,DIRAF:def 3;
    then consider e2 such that
A8: b,p // p,e2 and
A9: b,a // e1,e2 by A5,ANALOAF:def 5;
    Mid e1,p,a by A6,DIRAF:9;
    then
A10: e1,p // p,a by DIRAF:def 3;
A11: now
A12:  now
A13:    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:2,4;
        end;
        assume
A14:    a,b // b,p;
        then a,b // a,p by ANALOAF:def 5;
        then b,p // a,p or a=b by A14,ANALOAF:def 5;
        hence thesis by A13,DIRAF:1;
      end;
A15:  now
        assume
A16:    a,p // p,b;
        then a,p // a,b by ANALOAF:def 5;
        then a,b // p,b by A5,A16,ANALOAF:def 5;
        then b,a // b,p by DIRAF:2;
        hence p,a // p,p & b,a // c,p by A2,A3,DIRAF:3,4;
      end;
      assume p=e2;
      then b,a // p,a by A7,A10,A9,DIRAF:3;
      then a,b // a,p by DIRAF:2;
      hence thesis by A12,A15,DIRAF:6;
    end;
A17: now
A18:  now
        assume that
        p,a // a,b and
A19:    p,c // c,a;
        p,c // p,a by A19,ANALOAF:def 5;
        hence p,a // p,c & b,a // c,c by DIRAF:2,4;
      end;
A20:  now
        assume that
        p,b // b,a and
A21:    p,c // c,a;
        p,c // p,a by A21,ANALOAF:def 5;
        hence p,a // p,c & b,a // c,c by DIRAF:2,4;
      end;
A22:  now
        assume that
A23:    p,a // a,b and
A24:    p,a // a,c;
        a,b // a,c by A5,A23,A24,ANALOAF:def 5;
        hence p,a // p,a & b,a // c,a by DIRAF:1,2;
      end;
A25:  p,b // b,a & p,a // a,c implies p,a // p,c & b,a // c,c by ANALOAF:def 5;
      assume that
A26:  e1=e2 and
A27:  e2<>p;
      p,e2 // a,p by A10,A26,DIRAF:2;
      then b,p // a,p by A8,A27,DIRAF:3;
      then
A28:  p,b // p,a by DIRAF:2;
      then p,a // p,c by A1,A2,ANALOAF:def 5;
      hence thesis by A28,A25,A20,A22,A18,DIRAF:6;
    end;
    now
      assume that
A29:  e1<>e2 and
A30:  e2<>p;
      p,b // e2,p by A8,DIRAF:2;
      then e2,p // p,c by A1,A2,ANALOAF:def 5;
      then consider x such that
A31:  e1,p // p,x and
A32:  e1,e2 // c,x by A30,ANALOAF:def 5;
A33:  p,a // p,x by A7,A10,A31,ANALOAF:def 5;
      b,a // c,x by A9,A29,A32,DIRAF:3;
      hence thesis by A33;
    end;
    hence thesis by A17,A11;
  end;
A34: p=c implies p,a // p,c & b,a // c,c by DIRAF:4;
  p=a implies p,a // p,a & b,a // c,a by A1,DIRAF:1,2;
  hence thesis by A34,A4;
end;

theorem Th19:
  Mid p,c,b implies ex x st Mid p,x,a & b,a // c,x
proof
A1: b=c implies Mid p,a,a & b,a // c,a by DIRAF:1,10;
  assume
A2: Mid p,c,b;
A3: now
    assume p=b;
    then p=c by A2,DIRAF:8;
    hence Mid p,p,a & b,a // c,p by DIRAF:4,10;
  end;
A4: p,c // c,b by A2,DIRAF:def 3;
A5: now
    assume that
A6: p<>c and
A7: p<>b and
A8: b<>c;
    Mid b,c,p by A2,DIRAF:9;
    then
A9: b,c // c,p by DIRAF:def 3;
    then
A10: b,c // b,p by ANALOAF:def 5;
    then
A11: b,p // c,p by A8,A9,ANALOAF:def 5;
A12: now
A13:  now
        assume
A14:    Mid p,a,b;
A15:    now
          Mid b,a,p by A14,DIRAF:9;
          then b,a // a,p by DIRAF:def 3;
          then
A16:      a,p // b,a by DIRAF:2;
          assume Mid p,a,c;
          then Mid c,a,p by DIRAF:9;
          then c,a // a,p by DIRAF:def 3;
          then
A17:      a,p // c,a by DIRAF:2;
A18:      b,a // c,a implies Mid p,a,a & b,a // c,a by DIRAF:10;
          a=p implies Mid p,p,a & b,a // c,p by A8,A9,A10,ANALOAF:def 5
,DIRAF:10;
          hence thesis by A17,A16,A18,ANALOAF:def 5;
        end;
        Mid p,c,a implies Mid p,c,a & b,a // c,c by DIRAF:4;
        hence thesis by A2,A14,A15,DIRAF:17;
      end;
A19:  now
        assume Mid a,p,b;
        then Mid b,p,a by DIRAF:9;
        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 A7,A11,ANALOAF:def 5,DIRAF:10;
      end;
A20:  now
A21:    p,c // p,b by A4,ANALOAF:def 5;
        assume
A22:    Mid p,b,a;
        then p,b // b,a by DIRAF:def 3;
        then p,c // b,a by A7,A21,DIRAF:3;
        then b,a // c,b by A4,A6,ANALOAF:def 5;
        hence thesis by A22;
      end;
      assume LIN p,a,b;
      hence thesis by A13,A19,A20,DIRAF:29;
    end;
    now
A23:  p,b // p,c by A2,DIRAF:7;
      assume
A24:  not LIN p,a,b;
      then p<>b by DIRAF:31;
      then consider x such that
A25:  p,a // p,x and
A26:  b,a // c,x by A23,Th18;
A27:  p,x // p,a by A25,DIRAF:2;
      c,x // b,a by A26,DIRAF:2;
      hence thesis by A2,A6,A24,A26,A27,Th15;
    end;
    hence thesis by A12;
  end;
  p=c implies Mid p,p,a & b,a // c,p by DIRAF:4,10;
  hence thesis by A3,A1,A5;
end;

theorem Th20:
  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 and
A8: b,a // c,x by A1,A4,Th18;
A9: p<>c by A1,A2,DIRAF:8;
A10: p<>x
    proof
      p,b // p,c by A2,DIRAF:7;
      then
A11:  c,p // b,p by DIRAF:2;
      assume p=x;
      then b,a // b,p by A8,A9,A11,DIRAF:3;
      then Mid b,a,p or Mid b,p,a by DIRAF:7;
      then LIN b,a,p or LIN b,p,a by DIRAF:28;
      hence contradiction by A6,DIRAF:30;
    end;
    not LIN p,x,c
    proof
      Mid p,a,x or Mid p,x,a by A7,DIRAF:7;
      then LIN p,a,x or LIN p,x,a by DIRAF:28;
      then
A12:  LIN p,x,a by DIRAF:30;
A13:  LIN p,x,p by DIRAF:31;
      LIN p,b,c by A2,DIRAF:28;
      then
A14:  LIN p,c,b by DIRAF:30;
A15:  LIN p,c,p by DIRAF:31;
      assume LIN p,x,c;
      then LIN p,c,a by A10,A12,A13,DIRAF:32;
      hence contradiction by A6,A9,A14,A15,DIRAF:32;
    end;
    hence thesis by A1,A2,A7,A8,Th15;
  end;
A16: now
    assume that
A17: LIN p,a,b and
A18: c <>b;
A19: now
      assume Mid p,a,b;
      then Mid a,b,c by A2,DIRAF:11;
      then Mid c,b,a by DIRAF:9;
      then
A20:  c,b // b,a by DIRAF:def 3;
      then c,b // c,a by ANALOAF:def 5;
      hence Mid p,a,a & b,a // c,a by A18,A20,ANALOAF:def 5,DIRAF:10;
    end;
A21: now
      assume Mid p,b,a;
      then
A22:  p,b // b,a by DIRAF:def 3;
A23:  now
A24:    now
          assume p,a // a,c;
          then Mid p,a,c by DIRAF:def 3;
          hence thesis by DIRAF:4;
        end;
A25:    now
          assume a=b;
          then b,a // c,a by DIRAF:4;
          hence thesis by DIRAF:10;
        end;
        p,b // p,a by A22,ANALOAF:def 5;
        then
A26:    b,a // p,a by A1,A22,ANALOAF:def 5;
        assume b,a // a,c;
        hence thesis by A26,A25,A24,ANALOAF:def 5;
      end;
A27:  now
        assume
A28:    b,c // c,a;
        then b,c // b,a by ANALOAF:def 5;
        hence Mid p,a,a & b,a // c,a by A18,A28,ANALOAF:def 5,DIRAF:10;
      end;
      b,a // b,c by A1,A3,A22,ANALOAF:def 5;
      hence thesis by A23,A27,ANALOAF:def 5;
    end;
    now
      assume Mid a,p,b;
      then Mid a,b,c by A1,A2,DIRAF:12;
      then Mid c,b,a by DIRAF:9;
      then
A29:  c,b // b,a by DIRAF:def 3;
      then c,b // c,a by ANALOAF:def 5;
      hence Mid p,a,a & b,a // c,a by A18,A29,ANALOAF:def 5,DIRAF:10;
    end;
    hence thesis by A17,A19,A21,DIRAF:29;
  end;
  c =b implies Mid p,a,a & b,a // c,a by DIRAF:1,10;
  hence thesis by A5,A16;
end;

theorem Th21:
  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 by A1,DIRAF:31;
A4: LIN p,c,b by A2,DIRAF:28;
A5: Mid b,c,p by A2,DIRAF:9;
  then
A6: b,c // c,p by DIRAF:def 3;
A7: a<>b by A1,DIRAF:31;
A8: now
    assume that
A9: b<>c and
A10: a<>c and
A11: p<>c;
    consider e1 such that
A12: Mid b,e1,a and
A13: p,a // c,e1 by A5,Th19;
A14: not LIN p,c,a
    proof
A15:  LIN p,c,p by DIRAF:31;
      assume LIN p,c,a;
      hence contradiction by A1,A4,A11,A15,DIRAF:32;
    end;
A16: a<>e1
    proof
      assume a=e1;
      then a,p // a,c by A13,DIRAF:2;
      then Mid a,p,c or Mid a,c,p by DIRAF:7;
      then LIN a,p,c or LIN a,c,p by DIRAF:28;
      hence contradiction by A14,DIRAF:30;
    end;
    consider e4 such that
A17: e1,c // c,e4 and
A18: e1,b // p,e4 by A6,A9,ANALOAF:def 5;
    consider e2 such that
A19: a,c // c,e2 and
A20: a,b // p,e2 by A6,A9,ANALOAF:def 5;
    consider e3 such that
A21: p,c // c,e3 and
A22: p,a // e2,e3 by A10,A19,ANALOAF:def 5;
A23: not LIN a,b,c
    proof
      assume LIN a,b,c;
      then
A24:  LIN b,c,a by DIRAF:30;
A25:  LIN b,c,b by DIRAF:31;
      LIN b,c,p by A4,DIRAF:30;
      hence contradiction by A1,A9,A24,A25,DIRAF:32;
    end;
A26: c <>e2
    proof
      assume
A27:  c =e2;
      p,c // c,b by A6,DIRAF:2;
      then a,b // c,b by A11,A20,A27,DIRAF:3;
      then b,a // b,c by DIRAF:2;
      then Mid b,a,c or Mid b,c,a by DIRAF:7;
      then LIN b,a,c or LIN b,c,a by DIRAF:28;
      hence contradiction by A23,DIRAF:30;
    end;
A28: e2<>e3
    proof
      assume e2=e3;
      then c,e2 // p,c by A21,DIRAF:2;
      then a,c // p,c by A19,A26,DIRAF:3;
      then c,a // c,p by DIRAF:2;
      then Mid c,a,p or Mid c,p,a by DIRAF:7;
      then LIN c,a,p or LIN c,p,a by DIRAF:28;
      hence contradiction by A14,DIRAF:30;
    end;
A29: c <>e1
    proof
      assume c =e1;
      then LIN b,c,a by A12,DIRAF:28;
      hence contradiction by A23,DIRAF:30;
    end;
A30: p<>e4
    proof
      assume p=e4;
      then c,e1 // p,c by A17,DIRAF:2;
      then p,a // p,c by A13,A29,DIRAF:3;
      then Mid p,a,c or Mid p,c,a by DIRAF:7;
      then LIN p,a,c or LIN p,c,a by DIRAF:28;
      hence contradiction by A14,DIRAF:30;
    end;
    Mid e1,c,e4 by A17,DIRAF:def 3;
    then Mid e4,c,e1 by DIRAF:9;
    then
A31: e4,c // c,e1 by DIRAF:def 3;
    c,e1 // e2,e3 by A3,A13,A22,ANALOAF:def 5;
    then
A32: e4,c // e2,e3 by A29,A31,DIRAF:3;
A33: e2<>e4
    proof
      assume e2=e4;
      then c,e2 // e1,c by A17,DIRAF:2;
      then a,c // e1,c by A19,A26,DIRAF:3;
      then c,e1 // c,a by DIRAF:2;
      then p,a // c,a by A13,A29,DIRAF:3;
      then a,p // a,c by DIRAF:2;
      then Mid a,p,c or Mid a,c,p by DIRAF:7;
      then LIN a,p,c or LIN a,c,p by DIRAF:28;
      hence contradiction by A14,DIRAF:30;
    end;
A34: c <>e3
    proof
      assume c =e3;
      then c,e2 // a,p by A22,DIRAF:2;
      then a,c // a,p by A19,A26,DIRAF:3;
      then Mid a,c,p or Mid a,p,c by DIRAF:7;
      then LIN a,c,p or LIN a,p,c by DIRAF:28;
      hence contradiction by A14,DIRAF:30;
    end;
A35: p<>e3 by A11,A21,ANALOAF:def 5;
A36: not LIN p,e3,e2
    proof
      p,c // c,b by A2,DIRAF:def 3;
      then
A37:  p,c // p,b by ANALOAF:def 5;
      p,c // p,e3 by A21,ANALOAF:def 5;
      then p,b // p,e3 by A11,A37,ANALOAF:def 5;
      then Mid p,b,e3 or Mid p,e3,b by DIRAF:7;
      then LIN p,b,e3 or LIN p,e3,b by DIRAF:28;
      then
A38:  LIN p,e3,b by DIRAF:30;
A39:  LIN p,e3,p by DIRAF:31;
      a,c // a,e2 by A19,ANALOAF:def 5;
      then Mid a,c,e2 or Mid a,e2,c by DIRAF:7;
      then LIN a,c,e2 or LIN a,e2,c by DIRAF:28;
      then
A40:  LIN c,e2,a by DIRAF:30;
      p,c // p,e3 by A21,ANALOAF:def 5;
      then Mid p,c,e3 or Mid p,e3,c by DIRAF:7;
      then LIN p,c,e3 or LIN p,e3,c by DIRAF:28;
      then
A41:  LIN p,e3,c by DIRAF:30;
      assume LIN p,e3,e2;
      then LIN p,e3,a by A26,A41,A40,DIRAF:35;
      hence contradiction by A1,A35,A38,A39,DIRAF:32;
    end;
    then
A42: not LIN e3,e2,p by DIRAF:30;
    consider e5 such that
A43: e4,e2 // c,e5 and
A44: e4,c // e2,e5 and
A45: e2<>e5 by ANALOAF:def 5;
A46: b<>e1
    proof
      p,c // c,b by A2,DIRAF:def 3;
      then
A47:  c,b // p,c by DIRAF:2;
      assume b=e1;
      then p,a // p,c by A9,A13,A47,DIRAF:3;
      then Mid p,a,c or Mid p,c,a by DIRAF:7;
      then LIN p,a,c or LIN p,c,a by DIRAF:28;
      hence contradiction by A14,DIRAF:30;
    end;
A48: c <>e4
    proof
      assume
A49:  c =e4;
      p,c // c,b by A2,DIRAF:def 3;
      then e1,b // c,b by A11,A18,A49,DIRAF:3;
      then b,e1 // b,c by DIRAF:2;
      then Mid b,e1,c or Mid b,c,e1 by DIRAF:7;
      then LIN b,e1,c or LIN b,c,e1 by DIRAF:28;
      then
A50:  LIN b,e1,c by DIRAF:30;
A51:  LIN b,e1,b by DIRAF:31;
      LIN b,e1,a by A12,DIRAF:28;
      hence contradiction by A23,A46,A50,A51,DIRAF:32;
    end;
A52: c <>e5
    proof
      assume c =e5;
      then c,e4 // c,e2 by A44,DIRAF:2;
      then e1,c // c,e2 by A17,A48,DIRAF:3;
      then c,e2 // e1,c by DIRAF:2;
      then a,c // e1,c by A19,A26,DIRAF:3;
      then c,e1 // c,a by DIRAF:2;
      then p,a // c,a by A13,A29,DIRAF:3;
      then a,p // a,c by DIRAF:2;
      then Mid a,p,c or Mid a,c,p by DIRAF:7;
      then LIN a,p,c or LIN a,c,p by DIRAF:28;
      hence contradiction by A14,DIRAF:30;
    end;
    Mid a,e1,b by A12,DIRAF:9;
    then
A53: a,e1 // e1,b by DIRAF:def 3;
    then a,e1 // a,b by ANALOAF:def 5;
    then a,b // e1,b by A16,A53,ANALOAF:def 5;
    then e1,b // p,e2 by A7,A20,ANALOAF:def 5;
    then
A54: p,e4 // p,e2 by A18,A46,ANALOAF:def 5;
    Mid p,c,e3 by A21,DIRAF:def 3;
    then Mid p,e4,e2 by A36,A32,A30,A54,Th16;
    then
A55: p,e4 // e4,e2 by DIRAF:def 3;
    then p,e4 // p,e2 by ANALOAF:def 5;
    then
A56: p,e2 // e4,e2 by A30,A55,ANALOAF:def 5;
    then
A57: p,e2 // c,e5 by A43,A33,DIRAF:3;
    p<>e2
    proof
      assume p=e2;
      then Mid a,c,p by A19,DIRAF:def 3;
      hence contradiction by A14,DIRAF:9,28;
    end;
    then
A58: a,b // e4,e2 by A20,A56,DIRAF:3;
    then
A59: a,b // c,e5 by A43,A33,DIRAF:3;
A60: e5<>e3
    proof
      assume e5=e3;
      then c,e3 // a,b by A59,DIRAF:2;
      then p,c // a,b by A21,A34,DIRAF:3;
      then c,p // b,a by DIRAF:2;
      then b,c // b,a by A6,A11,DIRAF:3;
      then Mid b,c,a or Mid b,a,c by DIRAF:7;
      then LIN b,c,a or LIN b,a,c by DIRAF:28;
      hence contradiction by A23,DIRAF:30;
    end;
    c,e1 // e4,c by A17,DIRAF:2;
    then c,e1 // e2,e5 by A44,A48,DIRAF:3;
    then p,a // e2,e5 by A13,A29,DIRAF:3;
    then e2,e3 // e2,e5 by A3,A22,ANALOAF:def 5;
    then Mid e2,e3,e5 or Mid e2,e5,e3 by DIRAF:7;
    then LIN e2,e3,e5 or LIN e2,e5,e3 by DIRAF:28;
    then
A61: LIN e2,e3,e5 by DIRAF:30;
    Mid p,c,e3 by A21,DIRAF:def 3;
    then
A62: Mid e3,c,p by DIRAF:9;
    e3,c // c,p by A21,DIRAF:2;
    then consider x such that
A63: e5,c // c,x and
A64: e5,e3 // p,x by A34,ANALOAF:def 5;
A65: c,e5 // x,c by A63,DIRAF:2;
    Mid p,c,e3 by A21,DIRAF:def 3;
    then Mid e3,c,p by DIRAF:9;
    then e3,c // c,p by DIRAF:def 3;
    then e3,c // e3,p by ANALOAF:def 5;
    then e3,p // e3,c by DIRAF:2;
    then not Mid e2,e3,e5 by A60,A57,A42,Th17;
    then Mid e3,e2,e5 or Mid e2,e5,e3 by A61,DIRAF:29;
    then e3,e2 // e2,e5 or Mid e3,e5,e2 by DIRAF:9,def 3;
    then e3,e2 // e3,e5 or e3,e5 // e5,e2 by ANALOAF:def 5,DIRAF:def 3;
    then
A66: e3,e5 // e3,e2 by ANALOAF:def 5,DIRAF:2;
    c,e5 // p,e2 by A57,DIRAF:2;
    then Mid e3,e5,e2 by A34,A42,A66,A62,Th15;
    then Mid e2,e5,e3 by DIRAF:9;
    then
A67: e2,e5 // e5,e3 by DIRAF:def 3;
    then e2,e5 // e2,e3 by ANALOAF:def 5;
    then e2,e3 // e5,e3 by A45,A67,ANALOAF:def 5;
    then p,a // e5,e3 by A22,A28,DIRAF:3;
    then p,a // p,x by A64,A60,DIRAF:3;
    then
A68: p,x // p,a by DIRAF:2;
    a,b // c,e5 by A43,A33,A58,DIRAF:3;
    then
A69: a,b // x,c by A52,A65,DIRAF:3;
    then c,x // b,a by DIRAF:2;
    hence thesis by A1,A2,A11,A69,A68,Th15;
  end;
A70: a=c implies a,b // a,c & Mid p,a,a by DIRAF:4,10;
A71: p=c implies a,b // c,c & Mid p,c,a by DIRAF:4,10;
  b=c implies a,b // a,c & Mid p,a,a by DIRAF:1,10;
  hence thesis by A8,A70,A71;
end;

theorem
  ex x st a,x // b,c & a,b // x,c
proof
A1: now
    consider e3 such that
A2: Mid b,c,e3 and
A3: c <>e3 by DIRAF:13;
A4: b,c // c,e3 by A2,DIRAF:def 3;
    assume
A5: not LIN a,b,c;
    then
A6: b<>c by DIRAF:31;
    then consider e4 such that
A7: a,c // c,e4 and
A8: a,b // e3,e4 by A4,ANALOAF:def 5;
A9: Mid a,c,e4 by A7,DIRAF:def 3;
    then Mid e4,c,a by DIRAF:9;
    then
A10: e4,c // c,a by DIRAF:def 3;
A11: e4<>c
    proof
      assume
A12:  e4=c;
      e3,c // c,b by A4,DIRAF:2;
      then a,b // c,b by A3,A8,A12,DIRAF:3;
      then b,a // b,c by DIRAF:2;
      then Mid b,a,c or Mid b,c,a by DIRAF:7;
      then LIN b,a,c or LIN b,c,a by DIRAF:28;
      hence contradiction by A5,DIRAF:30;
    end;
A13: not LIN e4,c,e3
    proof
      LIN b,c,e3 by A2,DIRAF:28;
      then
A14:  LIN c,e3,b by DIRAF:30;
      assume
A15:  LIN e4,c,e3;
A16:  LIN c,e3,c by DIRAF:31;
A17:  LIN e4,c,c by DIRAF:31;
      LIN e4,c,a by A9,DIRAF:9,28;
      then LIN c,e3,a by A11,A15,A17,DIRAF:32;
      hence contradiction by A5,A3,A14,A16,DIRAF:32;
    end;
    b,c // c,e3 by A2,DIRAF:def 3;
    then
A18: c,e3 // b,c by DIRAF:2;
    consider e1 such that
A19: Mid c,a,e1 and
A20: a<>e1 by DIRAF:13;
A21: c,a // a,e1 by A19,DIRAF:def 3;
A22: a<>c by A5,DIRAF:31;
    then consider e2 such that
A23: b,a // a,e2 and
A24: b,c // e1,e2 by A21,ANALOAF:def 5;
    c,a // c,e1 by A21,ANALOAF:def 5;
    then e4,c // c,e1 by A22,A10,DIRAF:3;
    then
A25: Mid e4,c,e1 by DIRAF:def 3;
    then consider e5 such that
A26: Mid e4,e3,e5 and
A27: c,e3 // e1,e5 by A11,Th20;
A28: e4<>e3
    proof
      assume e4=e3;
      then Mid a,c,e3 by A7,DIRAF:def 3;
      then
A29:  LIN e3,c,a by DIRAF:9,28;
A30:  LIN e3,c,c by DIRAF:31;
      LIN e3,c,b by A2,DIRAF:9,28;
      hence contradiction by A5,A3,A29,A30,DIRAF:32;
    end;
    then
A31: e4<>e5 by A26,DIRAF:8;
A32: e1<>e4 by A25,A11,DIRAF:8;
A33: not LIN e1,e4,e3
    proof
      LIN e4,c,e1 by A25,DIRAF:28;
      then
A34:  LIN e4,e1,c by DIRAF:30;
      assume LIN e1,e4,e3;
      then
A35:  LIN e4,e1,e3 by DIRAF:30;
      LIN e4,e1,e4 by DIRAF:31;
      hence contradiction by A32,A13,A35,A34,DIRAF:32;
    end;
A36: not LIN e1,e5,e4
    proof
      LIN e4,e3,e5 by A26,DIRAF:28;
      then
A37:  LIN e5,e4,e3 by DIRAF:30;
      assume LIN e1,e5,e4;
      then
A38:  LIN e5,e4,e1 by DIRAF:30;
      LIN e5,e4,e4 by DIRAF:31;
      hence contradiction by A31,A33,A38,A37,DIRAF:32;
    end;
    then
A39: e1<>e5 by DIRAF:31;
    Mid e1,c,e4 by A25,DIRAF:9;
    then consider e6 such that
A40: Mid e1,e6,e5 and
A41: e5,e4 // e6,c by A36,Th21;
A42: c <>e1 by A19,A20,DIRAF:8;
A43: not LIN c,e1,b
    proof
      LIN c,a,e1 by A19,DIRAF:28;
      then
A44:  LIN c,e1,a by DIRAF:30;
A45:  LIN c,e1,c by DIRAF:31;
      assume LIN c,e1,b;
      hence contradiction by A5,A42,A44,A45,DIRAF:32;
    end;
A46: e5<>e3
    proof
      assume e5=e3;
      then e3,c // e3,e1 by A27,DIRAF:2;
      then Mid e3,c,e1 or Mid e3,e1,c by DIRAF:7;
      then LIN e3,c,e1 or LIN e3,e1,c by DIRAF:28;
      then
A47:  LIN e3,c,e1 by DIRAF:30;
A48:  LIN e3,c,c by DIRAF:31;
      LIN e3,c,b by A2,DIRAF:9,28;
      hence contradiction by A3,A43,A47,A48,DIRAF:32;
    end;
A49: e1<>e6
    proof
      Mid e5,e3,e4 by A26,DIRAF:9;
      then
A50:  e5,e3 // e3,e4 by DIRAF:def 3;
      then e5,e3 // e5,e4 by ANALOAF:def 5;
      then
A51:  e5,e4 // e3,e4 by A46,A50,ANALOAF:def 5;
      assume e1=e6;
      then e3,e4 // e1,c by A31,A41,A51,ANALOAF:def 5;
      then
A52:  a,b // e1,c by A8,A28,DIRAF:3;
      Mid e1,a,c by A19,DIRAF:9;
      then
A53:  e1,a // a,c by DIRAF:def 3;
      then e1,a // e1,c by ANALOAF:def 5;
      then e1,c // a,c by A20,A53,ANALOAF:def 5;
      then a,b // a,c by A42,A52,DIRAF:3;
      then a,b // b,c or a,c // c,b by DIRAF:6;
      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:28;
      hence contradiction by A5,DIRAF:30;
    end;
    consider x such that
A54: Mid c,x,e6 and
A55: e1,e6 // a,x by A19,Th19;
    e1,e6 // e6,e5 by A40,DIRAF:def 3;
    then e1,e6 // e1,e5 by ANALOAF:def 5;
    then e1,e5 // a,x by A55,A49,ANALOAF:def 5;
    then c,e3 // a,x by A27,A39,DIRAF:3;
    then
A56: a,x // b,c by A3,A18,ANALOAF:def 5;
A57: e6<>c
    proof
      assume e6=c;
      then x=c by A54,DIRAF:8;
      then c,a // c,b by A56,DIRAF:2;
      then Mid c,a,b or Mid c,b,a by DIRAF:7;
      then LIN c,a,b or LIN c,b,a by DIRAF:28;
      hence contradiction by A5,DIRAF:30;
    end;
A58: a<>e2
    proof
      assume
A59:  a=e2;
      e1,a // a,c by A21,DIRAF:2;
      then b,c // a,c by A20,A24,A59,DIRAF:3;
      then c,b // c,a by DIRAF:2;
      then Mid c,b,a or Mid c,a,b by DIRAF:7;
      then LIN c,b,a or LIN c,a,b by DIRAF:28;
      hence contradiction by A5,DIRAF:30;
    end;
A60: e6<>x
    proof
      assume e6=x;
      then e6,e1 // e6,a by A55,DIRAF:2;
      then Mid e6,e1,a or Mid e6,a,e1 by DIRAF:7;
      then LIN e6,e1,a or LIN e6,a,e1 by DIRAF:28;
      then
A61:  LIN e6,e1,a by DIRAF:30;
      LIN e1,e6,e5 by A40,DIRAF:28;
      then
A62:  LIN e6,e1,e5 by DIRAF:30;
      b,c // e1,e5 by A3,A4,A27,DIRAF:3;
      then e1,e2 // e1,e5 by A6,A24,ANALOAF:def 5;
      then Mid e1,e2,e5 or Mid e1,e5,e2 by DIRAF:7;
      then LIN e1,e2,e5 or LIN e1,e5,e2 by DIRAF:28;
      then
A63:  LIN e1,e5,e2 by DIRAF:30;
A64:  LIN e1,e5,e1 by DIRAF:31;
      Mid b,a,e2 by A23,DIRAF:def 3;
      then LIN b,a,e2 by DIRAF:28;
      then
A65:  LIN a,e2,b by DIRAF:30;
      LIN c,a,e1 by A19,DIRAF:28;
      then
A66:  LIN a,e1,c by DIRAF:30;
      LIN e6,e1,e1 by DIRAF:31;
      then LIN e1,e5,a by A49,A61,A62,DIRAF:32;
      then
A67:  LIN a,e1,e2 by A39,A63,A64,DIRAF:32;
A68:  LIN a,e2,a by DIRAF:31;
      LIN a,e1,a by DIRAF:31;
      then LIN a,e2,c by A20,A67,A66,DIRAF:32;
      hence contradiction by A5,A58,A65,A68,DIRAF:32;
    end;
    Mid e6,x,c by A54,DIRAF:9;
    then
A69: e6,x // x,c by DIRAF:def 3;
    then e6,x // e6,c by ANALOAF:def 5;
    then
A70: e6,c // x,c by A60,A69,ANALOAF:def 5;
    Mid e5,e3,e4 by A26,DIRAF:9;
    then
A71: e5,e3 // e3,e4 by DIRAF:def 3;
    then e5,e3 // e5,e4 by ANALOAF:def 5;
    then e3,e4 // e5,e4 by A46,A71,ANALOAF:def 5;
    then a,b // e5,e4 by A8,A28,DIRAF:3;
    then a,b // e6,c by A31,A41,DIRAF:3;
    then a,b // x,c by A57,A70,DIRAF:3;
    hence thesis by A56;
  end;
  now
A72: 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:2,4;
    end;
A73: now
      assume Mid b,a,c;
      then Mid c,a,b by DIRAF:9;
      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:2,4;
    end;
A74: Mid a,b,c implies a,b // b,c & a,b // b,c by DIRAF:def 3;
    assume LIN a,b,c;
    hence thesis by A74,A73,A72,DIRAF:29;
  end;
  hence thesis by A1;
end;

theorem Th23:
  a,b // c,d & not LIN a,b,c implies ex x st Mid a,x,d & Mid b,x,c
proof
  assume that
A1: a,b // c,d and
A2: not LIN a,b,c;
A3: now
    consider e1 such that
A4: a,b // d,e1 and
A5: a,d // b,e1 and
A6: b<>e1 by ANALOAF:def 5;
A7: a<>b by A2,DIRAF:31;
    then c,d // d,e1 by A1,A4,ANALOAF:def 5;
    then
A8: Mid c,d,e1 by DIRAF:def 3;
A9: a<>d
    proof
      assume a=d;
      then b,a // a,c by A1,DIRAF:2;
      then Mid b,a,c by DIRAF:def 3;
      then LIN b,a,c by DIRAF:28;
      hence contradiction by A2,DIRAF:30;
    end;
A10: not LIN a,b,d
    proof
A11:  now
        assume a,b // a,d;
        then c,d // a,d by A1,A7,ANALOAF:def 5;
        then d,c // d,a by DIRAF:2;
        then d,c '||' d,a by DIRAF:def 4;
        hence LIN d,c,a by DIRAF:def 5;
      end;
A12:  LIN d,a,a by DIRAF:31;
A13:  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:28;
        hence LIN d,c,a by DIRAF:30;
      end;
      assume
A14:  LIN a,b,d;
      then
A15:  LIN d,a,b by DIRAF:30;
      a,b '||' a,d by A14,DIRAF:def 5;
      then LIN d,a,c by A11,A13,DIRAF:30,def 4;
      hence contradiction by A2,A9,A12,A15,DIRAF:32;
    end;
    consider e2 such that
A16: c,d // b,e2 and
A17: c,b // d,e2 and
A18: d<>e2 by ANALOAF:def 5;
    assume
A19: c <>d;
    then a,b // b,e2 by A1,A16,DIRAF:3;
    then
A20: Mid a,b,e2 by DIRAF:def 3;
A21: not LIN c,d,b
    proof
A22:  now
        assume c,d // c,b;
        then a,b // c,b by A1,A19,DIRAF:3;
        then b,a // b,c by DIRAF:2;
        then Mid b,a,c or Mid b,c,a by DIRAF:7;
        then LIN b,a,c or LIN b,c,a by DIRAF:28;
        hence contradiction by A2,DIRAF:30;
      end;
      assume LIN c,d,b;
      then c,d '||' c,b by DIRAF:def 5;
      then c,d // c,b or c,d // b,c by DIRAF:def 4;
      then a,b // b,c by A1,A19,A22,DIRAF:3;
      then Mid a,b,c by DIRAF:def 3;
      hence contradiction by A2,DIRAF:28;
    end;
A23: LIN b,c,c by DIRAF:31;
A24: LIN d,a,a by DIRAF:31;
A25: c <>e1
    proof
      assume c =e1;
      then c,d // d,c by A1,A4,A7,ANALOAF:def 5;
      hence contradiction by A19,ANALOAF:def 5;
    end;
    not LIN c,b,e1
    proof
      LIN c,d,e1 by A8,DIRAF:28;
      then
A26:  LIN c,e1,d by DIRAF:30;
      assume LIN c,b,e1;
      then
A27:  LIN c,e1,b by DIRAF:30;
      LIN c,e1,c by DIRAF:31;
      hence contradiction by A25,A21,A27,A26,DIRAF:32;
    end;
    then consider x such that
A28: Mid c,x,b and
A29: b,e1 // x,d by A8,Th21;
A30: Mid b,x,c by A28,DIRAF:9;
    a,d // x,d by A5,A6,A29,DIRAF:3;
    then d,a // d,x by DIRAF:2;
    then Mid d,a,x or Mid d,x,a by DIRAF:7;
    then LIN d,a,x or LIN d,x,a by DIRAF:28;
    then
A31: LIN d,a,x by DIRAF:30;
A32: b<>c by A2,DIRAF:31;
A33: a<>e2
    proof
      assume a=e2;
      then a,b // b,a by A1,A19,A16,DIRAF:3;
      hence contradiction by A7,ANALOAF:def 5;
    end;
    not LIN a,d,e2
    proof
      LIN a,b,e2 by A20,DIRAF:28;
      then
A34:  LIN a,e2,b by DIRAF:30;
      assume LIN a,d,e2;
      then
A35:  LIN a,e2,d by DIRAF:30;
      LIN a,e2,a by DIRAF:31;
      hence contradiction by A33,A10,A35,A34,DIRAF:32;
    end;
    then consider y such that
A36: Mid a,y,d and
A37: d,e2 // y,b by A20,Th21;
A38: LIN b,c,b by DIRAF:31;
    c,b // y,b by A17,A18,A37,DIRAF:3;
    then b,c // b,y by DIRAF:2;
    then Mid b,c,y or Mid b,y,c by DIRAF:7;
    then LIN b,c,y or LIN b,y,c by DIRAF:28;
    then
A39: LIN b,c,y by DIRAF:30;
A40: LIN c,x,b by A28,DIRAF:28;
    then LIN b,c,x by DIRAF:30;
    then
A41: LIN x,y,c by A32,A39,A23,DIRAF:32;
    LIN a,y,d by A36,DIRAF:28;
    then LIN d,a,y by DIRAF:30;
    then
A42: LIN x,y,a by A9,A31,A24,DIRAF:32;
    LIN b,c,x by A40,DIRAF:30;
    then LIN x,y,b by A32,A39,A38,DIRAF:32;
    then Mid a,x,d by A2,A36,A42,A41,DIRAF:32;
    hence thesis by A30;
  end;
  now
    assume
A43: c =d;
    take x=c;
    thus Mid a,x,d & Mid b,x,c by A43,DIRAF:10;
  end;
  hence thesis by A3;
end;

theorem
  OAS is Fanoian
proof
  let a,b,c,d;
  assume that
A1: a,b // c,d and
  a,c // b,d and
A2: not LIN a,b,c;
  thus thesis by A1,A2,Th23;
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 that
A1: a,b '||' c,d and
A2: a,c '||' b,d and
A3: not LIN a,b,c;
  a,b // c,d by A1,A2,A3,Th14;
  then consider x such that
A4: Mid a,x,d and
A5: Mid b,x,c by A3,Th23;
  LIN b,x,c by A5,DIRAF:28;
  then
A6: LIN x,b,c by DIRAF:30;
  LIN a,x,d by A4,DIRAF:28;
  then LIN x,a,d by DIRAF:30;
  hence thesis by A6;
end;

theorem
  a,b '||' c,d & not LIN a,b,c & LIN p,a,d & LIN p,b,c implies not LIN p ,a,b
proof
  assume that
A1: a,b '||' c,d and
A2: not LIN a,b,c and
A3: LIN p,a,d and
A4: LIN p,b,c;
A5: LIN p,a,a by DIRAF:31;
  assume LIN p,a,b;
  then
A6: LIN a,b,d by A2,A3,A4,A5,DIRAF:32;
A7: a,b '||' d,c by A1,DIRAF:22;
  a<>b by A2,DIRAF:31;
  hence contradiction by A2,A6,A7,DIRAF:33;
end;

theorem Th27:
  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 that
A1: Mid a,b,d and
A2: Mid b,x,c and
A3: not LIN a,b,c;
A4: now
    assume
A5: b=d;
    take y=c;
    thus Mid a,y,c & Mid d,x,y by A2,A5,DIRAF:10;
    thus Mid a,y,c & Mid y,x,d by A2,A5,DIRAF:9,10;
  end;
A6: Mid d,b,a by A1,DIRAF:9;
A7: now
    assume that
A8: b<>d and
A9: x<>b;
    d,b // b,a by A6,DIRAF:def 3;
    then consider e1 such that
A10: x,b // b,e1 and
A11: x,d // a,e1 by A8,ANALOAF:def 5;
A12: Mid x,b,e1 by A10,DIRAF:def 3;
    then
A13: Mid e1,b,x by DIRAF:9;
    then
A14: Mid e1,x,c by A2,A9,DIRAF:12;
A15: c <>e1
    proof
      assume c =e1;
      then Mid x,b,x by A2,A9,A13,DIRAF:8,12;
      hence contradiction by A9,DIRAF:8;
    end;
A16: x<>e1 by A9,A12,DIRAF:8;
A17: not LIN c,a,e1
    proof
      LIN x,b,e1 by A12,DIRAF:28;
      then
A18:  LIN x,e1,b by DIRAF:30;
      assume LIN c,a,e1;
      then
A19:  LIN c,e1,a by DIRAF:30;
      LIN c,x,e1 by A14,DIRAF:9,28;
      then
A20:  LIN c,e1,x by DIRAF:30;
A21:  LIN c,e1,c by DIRAF:31;
      LIN c,e1,e1 by DIRAF:31;
      then LIN c,e1,b by A16,A20,A18,DIRAF:35;
      hence contradiction by A3,A15,A19,A21,DIRAF:32;
    end;
    Mid c,x,e1 by A14,DIRAF:9;
    then consider y such that
A22: Mid c,y,a and
A23: a,e1 // y,x by A17,Th21;
    a<>e1 by A17,DIRAF:31;
    then x,d // y,x by A11,A23,DIRAF:3;
    then d,x // x,y by DIRAF:2;
    then Mid d,x,y by DIRAF:def 3;
    then
A24: Mid y,x,d by DIRAF:9;
    Mid a,y,c by A22,DIRAF:9;
    hence thesis by A24;
  end;
  now
    assume that
    b<>d and
A25: x=b;
    take y=a;
    thus Mid a,y,c & Mid y,x,d by A1,A25,DIRAF:10;
  end;
  hence thesis by A7,A4;
end;

theorem
  OAS is satisfying_Ext_Bet_Pasch
proof
  let a,b,c,d,x,y;
  assume that
A1: Mid a,b,d and
A2: Mid b,x,c and
A3: not LIN a,b,c;
  thus thesis by A1,A2,A3,Th27;
end;

theorem Th29:
  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: b<>c by A3,DIRAF:31;
A5: a<>b by A3,DIRAF:31;
A6: now
    assume that
A7: b<>d and
A8: x<>c and
A9: a<>x;
A10: a<>d by A1,A7,DIRAF:8;
    consider e1 such that
A11: Mid a,d,e1 and
A12: x,d // c,e1 by A2,A9,Th20;
A13: Mid e1,d,a by A11,DIRAF:9;
A14: LIN d,b,a by A1,DIRAF:9,28;
A15: not LIN a,x,b
    proof
A16:  LIN a,x,a by DIRAF:31;
      assume
A17:  LIN a,x,b;
      LIN a,x,c by A2,DIRAF:28;
      hence contradiction by A3,A9,A17,A16,DIRAF:32;
    end;
A18: not LIN x,d,a
    proof
      assume LIN x,d,a;
      then
A19:  LIN d,a,x by DIRAF:30;
A20:  LIN d,a,a by DIRAF:31;
      LIN d,a,b by A14,DIRAF:30;
      hence contradiction by A10,A15,A19,A20,DIRAF:32;
    end;
    then
A21: x<>d by DIRAF:31;
A22: Mid d,b,a by A1,DIRAF:9;
    Mid b,d,e1 by A1,A11,DIRAF:11;
    then Mid e1,d,b by DIRAF:9;
    then Mid e1,b,a by A22,A13,DIRAF:12;
    then
A23: e1,b // b,a by DIRAF:def 3;
    e1<>b by A7,A22,A13,DIRAF:14;
    then consider e2 such that
A24: c,b // b,e2 and
A25: c,e1 // a,e2 by A23,ANALOAF:def 5;
A26: Mid c,b,e2 by A24,DIRAF:def 3;
    then
A27: LIN c,b,e2 by DIRAF:28;
    Mid c,x,a by A2,DIRAF:9;
    then consider y such that
A28: Mid c,y,e2 and
A29: a,e2 // x,y by Th19;
A30: Mid c,b,y or Mid c,y,b by A26,A28,DIRAF:17;
A31: c <>e2 by A4,A24,ANALOAF:def 5;
A32: now
      LIN c,b,e2 by A26,DIRAF:28;
      then
A33:  LIN c,e2,b by DIRAF:30;
      LIN c,y,e2 by A28,DIRAF:28;
      then
A34:  LIN c,e2,y by DIRAF:30;
      LIN c,e2,c by DIRAF:31;
      then
A35:  LIN b,y,c by A31,A34,A33,DIRAF:32;
      LIN a,x,c by A2,DIRAF:28;
      then
A36:  LIN x,a,c by DIRAF:30;
A37:  Mid c,x,a by A2,DIRAF:9;
      assume
A38:  Mid x,d,y;
      then consider c9 such that
A39:  Mid x,c9,a and
A40:  Mid c9,b,y by A22,A18,Th27;
      LIN x,c9,a by A39,DIRAF:28;
      then
A41:  LIN x,a,c9 by DIRAF:30;
A42:  b<>y
      proof
        assume b=y;
        then LIN x,d,b by A38,DIRAF:28;
        then
A43:    LIN d,b,x by DIRAF:30;
A44:    LIN d,b,b by DIRAF:31;
        LIN a,x,c by A2,DIRAF:28;
        then LIN d,b,c by A9,A14,A43,DIRAF:35;
        hence contradiction by A3,A7,A14,A44,DIRAF:32;
      end;
      LIN c9,b,y by A40,DIRAF:28;
      then
A45:  LIN b,y,c9 by DIRAF:30;
      then
A46:  LIN c,c9,c by A42,A35,DIRAF:32;
      LIN b,y,b by DIRAF:31;
      then
A47:  LIN c,c9,b by A42,A35,A45,DIRAF:32;
      LIN x,a,a by DIRAF:31;
      then LIN c,c9,a by A9,A36,A41,DIRAF:32;
      then Mid x,c,a by A3,A39,A47,A46,DIRAF:32;
      hence contradiction by A8,A37,DIRAF:14;
    end;
A48: a<>e2
    proof
      assume a=e2;
      then Mid c,b,a by A24,DIRAF:def 3;
      hence contradiction by A3,DIRAF:9,28;
    end;
A49: LIN e1,d,a by A11,DIRAF:9,28;
A50: c <>e1
    proof
      assume c =e1;
      then
A51:  LIN d,a,c by A49,DIRAF:30;
A52:  LIN d,a,a by DIRAF:31;
      LIN d,a,b by A14,DIRAF:30;
      hence contradiction by A3,A10,A51,A52,DIRAF:32;
    end;
    then x,d // a,e2 by A12,A25,DIRAF:3;
    then x,d // x,y by A48,A29,DIRAF:3;
    then
A53: Mid x,d,y or Mid x,y,d by DIRAF:7;
    then
A54: Mid d,y,x by A32,DIRAF:9;
    now
A55:  b<>e2
      proof
A56:    a,b // b,d by A1,DIRAF:def 3;
        assume
A57:    b=e2;
        c,e1 // x,d by A12,DIRAF:2;
        then a,b // x,d by A25,A50,A57,ANALOAF:def 5;
        then x,d // b,d by A5,A56,ANALOAF:def 5;
        then d,x // d,b by DIRAF:2;
        then Mid d,x,b or Mid d,b,x by DIRAF:7;
        then LIN d,x,b or LIN d,b,x by DIRAF:28;
        then
A58:    LIN d,b,x by DIRAF:30;
        LIN d,b,b by DIRAF:31;
        then
A59:    LIN a,x,b by A7,A14,A58,DIRAF:32;
A60:    LIN a,x,c by A2,DIRAF:28;
        LIN a,x,a by A7,A14,A58,DIRAF:32;
        hence contradiction by A3,A9,A59,A60,DIRAF:32;
      end;
A61:  LIN b,d,a by A14,DIRAF:30;
A62:  y<>d
      proof
A63:    LIN c,e2,c by DIRAF:31;
A64:    LIN c,e2,b by A27,DIRAF:30;
        assume y=d;
        then LIN c,d,e2 by A28,DIRAF:28;
        then LIN c,e2,d by DIRAF:30;
        then LIN c,e2,a by A7,A14,A64,DIRAF:35;
        hence contradiction by A3,A31,A64,A63,DIRAF:32;
      end;
A65:  LIN b,e2,c by A27,DIRAF:30;
      assume
A66:  not Mid c,y,b;
      then
A67:  y<>b by DIRAF:10;
      Mid b,y,e2 by A28,A30,A66,DIRAF:11;
      then consider z such that
A68:  Mid b,d,z and
A69:  y,d // e2,z by A67,Th20;
A70:  LIN a,e2,a by DIRAF:31;
A71:  now
        assume
A72:    a=z;
        Mid d,b,a by A1,DIRAF:9;
        hence contradiction by A7,A68,A72,DIRAF:14;
      end;
      d,y // y,x by A54,DIRAF:def 3;
      then d,y // d,x by ANALOAF:def 5;
      then y,d // x,d by DIRAF:2;
      then y,d // c,e1 by A12,A21,DIRAF:3;
      then c,e1 // e2,z by A69,A62,ANALOAF:def 5;
      then a,e2 // e2,z by A25,A50,ANALOAF:def 5;
      then Mid a,e2,z by DIRAF:def 3;
      then LIN a,e2,z by DIRAF:28;
      then
A73:  LIN a,z,e2 by DIRAF:30;
A74:  LIN b,d,z by A68,DIRAF:28;
      then
A75:  LIN a,z,a by A7,A61,DIRAF:32;
      LIN b,d,b by DIRAF:31;
      then LIN a,z,b by A7,A74,A61,DIRAF:32;
      then
A76:  LIN a,e2,b by A73,A75,A71,DIRAF:32;
      LIN a,e2,e2 by A73,A75,A71,DIRAF:32;
      then LIN a,e2,c by A55,A76,A65,DIRAF:35;
      hence contradiction by A3,A48,A76,A70,DIRAF:32;
    end;
    then Mid b,y,c by DIRAF:9;
    hence thesis by A53,A32;
  end;
A77: b=d implies Mid b,d,c & Mid x,d,d by DIRAF:10;
A78: x=c implies Mid b,c,c & Mid x,c,d by DIRAF:10;
  a=x implies Mid b,b,c & Mid x,b,d by A1,DIRAF:10;
  hence thesis by A6,A77,A78;
end;

theorem
  OAS is satisfying_Int_Bet_Pasch
proof
  let a,b,c,d,x,y;
  assume that
A1: Mid a,b,d and
A2: Mid a,x,c and
A3: not LIN a,b,c;
  thus thesis by A1,A2,A3,Th29;
end;

theorem
  Mid p,a,b & p,a // p9,a9 & not LIN p,a,p9 & LIN p9,a9,b9 & p,p9 // a,
  a9 & p,p9 // b,b9 implies Mid p9,a9,b9
proof
  assume that
A1: Mid p,a,b and
A2: p,a // p9,a9 and
A3: not LIN p,a,p9 and
A4: LIN p9,a9,b9 and
A5: p,p9 // a,a9 and
A6: p,p9 // b,b9;
A7: p<>a by A3,DIRAF:31;
A8: p<>p9 by A3,DIRAF:31;
A9: LIN p,a,b by A1,DIRAF:28;
  then
A10: LIN p,b,a by DIRAF:30;
  now
A11: p<>b by A1,A7,DIRAF:8;
A12: p9<>b9
    proof
      assume
A13:  p9=b9;
      then b9,p // b9,b by A6,DIRAF:2;
      then Mid b9,p,b or Mid b9,b,p by DIRAF:7;
      then LIN b9,p,b or LIN b9,b,p by DIRAF:28;
      then
A14:  LIN p,b,b9 by DIRAF:30;
      LIN p,b,p by DIRAF:31;
      hence contradiction by A3,A10,A11,A13,A14,DIRAF:32;
    end;
A15: not LIN p,a,a9
    proof
      assume
A16:  LIN p,a,a9;
      p,a '||' a9,p9 by A2,DIRAF:def 4;
      hence contradiction by A3,A7,A16,DIRAF:33;
    end;
    then
A17: a<>a9 by DIRAF:31;
A18: now
      a,a9 // p,p9 by A5,DIRAF:2;
      then
A19:  a,a9 '||' p9,p by DIRAF:def 4;
      assume LIN a,a9,p9;
      then LIN a,a9,p by A17,A19,DIRAF:33;
      hence contradiction by A15,DIRAF:30;
    end;
    assume that
A20: p9<>a9 and
    a9<>b9;
    consider x such that
A21: Mid p,x,b9 and
A22: b,b9 // a,x by A1,Th19;
    Mid b9,x,p by A21,DIRAF:9;
    then consider y such that
A23: Mid b9,y,p9 and
A24: p,p9 // x,y by Th19;
    LIN b9,y,p9 by A23,DIRAF:28;
    then
A25: LIN p9,b9,y by DIRAF:30;
A26: b<>b9
    proof
      assume b=b9;
      then LIN a9,p9,b by A4,DIRAF:30;
      then a9,p9 '||' a9,b by DIRAF:def 5;
      then a9,p9 // a9,b or a9,p9 // b,a9 by DIRAF:def 4;
      then p9,a9 // a9,b or p9,a9 // b,a9 by DIRAF:2;
      then p,a // a9,b or p,a // b,a9 by A2,A20,DIRAF:3;
      then p,a '||' b,a9 by DIRAF:def 4;
      hence contradiction by A1,A7,A15,DIRAF:28,33;
    end;
A27: x<>a
    proof
      assume x=a;
      then
A28:  LIN p,a,b9 by A21,DIRAF:28;
      LIN p,a,a by DIRAF:31;
      then
A29:  LIN b,b9,a by A7,A9,A28,DIRAF:32;
      LIN p,a,p by DIRAF:31;
      then
A30:  LIN b,b9,p by A7,A9,A28,DIRAF:32;
      b,b9 // p,p9 by A6,DIRAF:2;
      then b,b9 '||' p,p9 by DIRAF:def 4;
      then LIN b,b9,p9 by A26,A30,DIRAF:33;
      hence contradiction by A3,A26,A29,A30,DIRAF:32;
    end;
A31: LIN p9,b9,a9 by A4,DIRAF:30;
    then
A32: LIN y,a9,a9 by A12,A25,DIRAF:32;
A33: p,p9 // a,x by A6,A22,A26,DIRAF:3;
    then a,x // x,y by A8,A24,ANALOAF:def 5;
    then a,x // a,y by ANALOAF:def 5;
    then p,p9 // a,y by A27,A33,DIRAF:3;
    then a,y // a,a9 by A5,A8,ANALOAF:def 5;
    then a,y '||' a,a9 by DIRAF:def 4;
    then LIN a,y,a9 by DIRAF:def 5;
    then
A34: LIN y,a9,a by DIRAF:30;
    LIN p9,b9,p9 by DIRAF:31;
    then LIN y,a9,p9 by A12,A25,A31,DIRAF:32;
    then y=a9 or LIN a,a9,p9 by A34,A32,DIRAF:32;
    hence thesis by A23,A18,DIRAF:9;
  end;
  hence thesis by DIRAF:10;
end;