The Mizar article:

Classical Configurations in Affine Planes

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

Received April 13, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: AFF_2
[ MML identifier index ]


environ

 vocabulary DIRAF, AFF_1, ANALOAF, INCSP_1, AFF_2;
 notation STRUCT_0, ANALOAF, DIRAF, AFF_1;
 constructors AFF_1, XBOOLE_0;
 clusters ZFMISC_1, XBOOLE_0;
 theorems AFF_1;

begin

reserve AP for AffinPlane;
reserve a,a',b,b',c,c',x,y,o,p,q,r,s
                     for Element of AP;
reserve A,C,C',D,K,M,N,P,T
             for Subset of AP;

definition let AP;
  attr AP is satisfying_PPAP means
  :Def1: for M,N,a,b,c,a',b',c' st M is_line & N is_line & a in M &
   b in M & c in M & a' in N & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b' holds a,c' // c,a';
  synonym AP satisfies_PPAP;
end;

definition let AP be AffinSpace;
  attr AP is Pappian means
  :Def2:
   for M,N being Subset of AP,
    o,a,b,c,a',b',c' being Element of AP
     st M is_line & N is_line & M<>N &
   o in M & o in N & o<>a & o<>a' & o<>b & o<>b' & o<>c & o<>c' & a in M &
   b in M & c in M & a' in N & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b' holds a,c' // c,a';
  synonym AP satisfies_PAP;
end;

definition let AP;
  attr AP is satisfying_PAP_1 means
  :Def3: for M,N,o,a,b,c,a',b',c' st M is_line & N is_line & M<>N &
   o in M & o in N & o<>a & o<>a' & o<>b & o<>b' & o<>c & o<>c' &
   a in M & b in M & c in M & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b<>c holds a' in N;
  synonym AP satisfies_PAP_1;
end;

definition let AP be AffinSpace;
 attr AP is Desarguesian means
  :Def4: for A,P,C being Subset of AP,
     o,a,b,c,a',b',c'  being Element of AP
    st o in A & o in P & o in C &
   o<>a & o<>b & o<>c & a in A & a' in A & b in P & b' in P &
   c in C & c' in C & A is_line & P is_line & C is_line &
   A<>P & A<>C & a,b // a',b' & a,c // a',c' holds b,c // b',c';
  synonym AP satisfies_DES;
end;

definition let AP;
 attr AP is satisfying_DES_1 means
  :Def5: for A,P,C,o,a,b,c,a',b',c' st o in A & o in P &
   o<>a & o<>b & o<>c & a in A & a' in A & b in P & b' in P &
   c in C & c' in C & A is_line & P is_line & C is_line &
   A<>P & A<>C & a,b // a',b' & a,c // a',c' & b,c // b',c' &
   not LIN a,b,c & c <>c' holds o in C;
  synonym AP satisfies_DES_1;
end;

definition let AP;
 attr AP is satisfying_DES_2 means
     for A,P,C,o,a,b,c,a',b',c' st o in A & o in P & o in C &
     o<>a & o<>b & o<>c & a in A & a' in A & b in P & b' in P & c in C &
     A is_line & P is_line & C is_line & A<>P & A<>C &
     a,b // a',b' & a,c // a',c' & b,c // b',c' holds c' in C;
  synonym AP satisfies_DES_2;
end;

definition let AP be AffinSpace;
 attr AP is Moufangian means
  :Def7: for K being Subset of AP,
      o,a,b,c,a',b',c'  being Element of AP
     st K is_line & o in K & c in K & c' in K &
    not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' &
    a,c // a',c' & a,b // K holds b,c // b',c';
  synonym AP satisfies_TDES;
end;

definition let AP;
 attr AP is satisfying_TDES_1 means
  :Def8: for K,o,a,b,c,a',b',c' st K is_line & o in K & c in K & c' in K &
   not a in K & o<>c & a<>b & LIN o,a,a' & a,b // a',b' & b,c // b',c' &
   a,c // a',c' & a,b // K holds LIN o,b,b';
  synonym AP satisfies_TDES_1;
end;

definition let AP;
 attr AP is satisfying_TDES_2 means
 :Def9: for K,o,a,b,c,a',b',c' st K is_line & o in K & c in K & c' in K &
  not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' & b,c // b',c' &
  a,c // a',c' & a,b // K holds a,b // a',b';
  synonym AP satisfies_TDES_2;
end;

definition let AP;
 attr AP is satisfying_TDES_3 means
  :Def10: for K,o,a,b,c,a',b',c' st K is_line & o in K & c in K &
   not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' &
    a,c // a',c' & b,c // b',c' & a,b // K holds c' in K;
  synonym AP satisfies_TDES_3;
end;

definition let AP be AffinSpace;
 attr AP is translational means
  :Def11: for A,P,C being Subset of AP,
     a,b,c,a',b',c'  being Element of AP
    st A // P & A // C & a in A & a' in A &
    b in P & b' in P & c in C & c' in C & A is_line & P is_line &
    C is_line & A<>P & A<>C & a,b // a',b' & a,c // a',c'
                                                holds b,c // b',c';
  synonym AP satisfies_des;
end;

definition let AP;
 attr AP is satisfying_des_1 means
  :Def12: for A,P,C,a,b,c,a',b',c' st A // P & a in A & a' in A & b in P &
   b' in P & c in C & c' in C & A is_line & P is_line & C is_line &
   A<>P & A<>C & a,b // a',b' & a,c // a',c' & b,c // b',c' &
   not LIN a,b,c & c <>c' holds A // C;
  synonym AP satisfies_des_1;
end;

definition let AP be AffinSpace;
 attr AP is satisfying_pap means
  :Def13: for M,N being Subset of AP,
     a,b,c,a',b',c'  being Element of AP
    st M is_line & N is_line &
   a in M & b in M & c in M & M // N & M<>N & a' in N & b' in N & c' in N &
    a,b' // b,a' & b,c' // c,b' holds a,c' // c,a';
  synonym AP satisfies_pap;
end;

definition let AP;
 attr AP is satisfying_pap_1 means
 :Def14: for M,N,a,b,c,a',b',c' st M is_line & N is_line &
  a in M & b in M & c in M & M // N & M<>N & a' in N & b' in N & a,b' // b,a' &
     b,c' // c,b' & a,c' // c,a' & a'<>b' holds c' in N;
  synonym AP satisfies_pap_1;
end;

canceled 14;

theorem
   AP satisfies_PAP iff AP satisfies_PAP_1
  proof
    A1: now assume A2: AP satisfies_PAP;
         thus AP satisfies_PAP_1
          proof let M,N,o,a,b,c,a',b',c';
           assume A3: M is_line & N is_line & M<>N & o in M &
            o in N & o<>a & o<>a' & o<>b & o<>b' & o<>c & o<>c' &
            a in M & b in M & c in M & b' in N & c' in N &
            a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b<>c;
           assume A4: not a' in N;
           A5: a<>b' & a<>c' by A3,AFF_1:30;
           A6: b<>a' proof assume b=a';
            then c,b // a,c' by A3,AFF_1:13; then c' in M by A3,AFF_1:62;
            hence contradiction by A3,AFF_1:30; end;
             not b,a' // N proof assume b,a' // N;
            then b,a' // N & b,a' // a,b' by A3,AFF_1:13;
            then a,b' // N by A6,AFF_1:46; then b',a // N by AFF_1:48;
            then a in N by A3,AFF_1:37;
            hence contradiction by A3,AFF_1:30; end; then consider
           x such that A7: x in N & LIN b,a',x by A3,AFF_1:73;
           A8: a,b' // b,x proof b,a' // b,x by A7,AFF_1:def 1;
            hence thesis by A3,A6,AFF_1:14; end;
           A9: o<>x proof assume o=x;
            then b,o // a,b' by A8,AFF_1:13; then b' in M by A3,AFF_1:62;
            hence contradiction by A3,AFF_1:30; end;
           then a,c' // c,x by A2,A3,A7,A8,Def2;
           then c,a' // c,x by A3,A5,AFF_1:14; then LIN c,a',x by AFF_1:def 1
;
           then LIN a',x,c & LIN a',x,b & LIN a',x,x by A7,AFF_1:15,16;
           then LIN b,c,x by A4,A7,AFF_1:17; then x in M by A3,AFF_1:39;
          hence contradiction by A3,A7,A9,AFF_1:30; end;
        end;
       now assume A10: AP satisfies_PAP_1;
         thus AP satisfies_PAP
          proof let M,N,o,a,b,c,a',b',c';
           assume A11: M is_line & N is_line & M<>N & o in M &
            o in N & o<>a & o<>a' & o<>b & o<>b' & o<>c &
            o<>c' & a in M & b in M & c in M & a' in N &
            b' in N & c' in N & a,b' // b,a' & b,c' // c,b';
           assume A12: not a,c' // c,a';
           then A13: a<>c' & c <>a' by AFF_1:12;
           A14: a<>b' & b<>a' by A11,AFF_1:30;
           A15: b<>c proof assume A16: b=c;
            then LIN b,c',b' by A11,AFF_1:def 1; then LIN
 b',c',b by AFF_1:15;
            then b'=c' or b in N by A11,AFF_1:39;
            hence contradiction by A11,A12,A16,AFF_1:30; end;
           A17: b'<>c' proof assume b'=c';
            then b',b // b',c by A11,AFF_1:13; then LIN b',b,c by AFF_1:def 1
;
            then LIN b,c,b' by AFF_1:15; then b' in M by A11,A15,AFF_1:39;
            hence contradiction by A11,AFF_1:30; end;
           set A=Line(a,c'), P=Line(b,a');
           A18: A is_line & P is_line & a in A & c' in A &
            b in P & a' in P by A13,A14,AFF_1:38; then consider K
           such that A19: c in K & A // K by AFF_1:63;
           A20: K is_line & K // A by A19,AFF_1:50;
             not P // K proof assume P // K;
            then P // A by A19,AFF_1:58;
            then b,a' // a,c' by A18,AFF_1:53;
            then a,b' // a,c' by A11,A14,AFF_1:14; then LIN a,b',c' by AFF_1:
def 1;
            then LIN b',c',a by AFF_1:15;
            then a in N by A11,A17,AFF_1:39;
            hence contradiction by A11,AFF_1:30; end;
           then consider x such that
           A21: x in P & x in K by A18,A20,AFF_1:72;
           A22: a,c' // c,x by A18,A19,A21,AFF_1:53;
              a,b' // b,x proof LIN b,x,a' by A18,A21,AFF_1:33;
            then b,x // b,a' by AFF_1:def 1; hence thesis by A11,A14,AFF_1:14
; end;
           then x in N by A10,A11,A15,A22,Def3; then N=P by A11,A12,A18,A21,A22
,AFF_1:30;
          hence contradiction by A11,A18,AFF_1:30; end;
        end;
   hence thesis by A1;
  end;

theorem
   AP satisfies_DES iff AP satisfies_DES_1
  proof
    A1: now assume A2: AP satisfies_DES;
         thus AP satisfies_DES_1
          proof let A,P,C,o,a,b,c,a',b',c';
            assume A3: o in A & o in P & o<>a & o<>b & o<>c &
            a in A & a' in A & b in P & b' in P & c in C &
            c' in C & A is_line & P is_line & C is_line &
            A<>P & A<>C & a,b // a',b' & a,c // a',c' &
            b,c // b',c' & not LIN a,b,c & c <>c';
            assume A4: not o in C; set K=Line(o,c');
            A5: K is_line & o in K & c' in K by A3,A4,AFF_1:38;
            A6: a<>b & a<>c & b<>c by A3,AFF_1:16;
            A7: a'<>c' proof assume A8: a'=c';
             then b,c // a',b' by A3,AFF_1:13;
              then a,b // b,c or a'=b' by A3,AFF_1:14;
             then b,a // b,c or a'=b' by AFF_1:13;
             then LIN b,a,c or a'=b' by AFF_1:def 1;
             hence contradiction by A3,A4,A8,AFF_1:15,30; end;
            A9: b'<>c' proof assume b'=c';
             then a'=b' or a,c // a,b by A3,AFF_1:14;
             then a'=b' or LIN a,c,b by AFF_1:def 1;
             then b,c // a,c by A3,A7,AFF_1:14,15; then c,b // c,a
               by AFF_1:13;
             then LIN c,b,a by AFF_1:def 1;
             hence contradiction by A3,AFF_1:15; end;
            A10: A<>K proof assume A=K;
             then c' in A & a',c' // a,c by A3,AFF_1:13,38;
             then c in A & c' in A by A3,A7,AFF_1:62;
             hence contradiction by A3,AFF_1:30; end;
              not a,c // K proof assume a,c // K;
             then a',c' // K by A3,A6,AFF_1:46;
             then c',a' // K by AFF_1:48; then a' in K by A5,AFF_1:37;
             then A11: a' in P by A3,A5,A10,AFF_1:30;
               a',b' // b,a by A3,AFF_1:13;
             then a'=b' or a in P by A3,A11,AFF_1:62;
             then a,c // b,c by A3,A7,AFF_1:14,30
; then c,a // c,b by AFF_1:13;
             then LIN c,a,b by AFF_1:def 1
; hence contradiction by A3,AFF_1:15; end;
             then consider x such that
            A12: x in K & LIN a,c,x by A5,AFF_1:73;
            A13: a,c // a,x by A12,AFF_1:def 1;
            then A14: a,x // a',c' by A3,A6,AFF_1:14;
            A15: not LIN a,b,x proof assume LIN a,b,x;
             then a,b // a,x by AFF_1:def 1;
             then a,b // a,c or a=x by A13,AFF_1:14;
             hence contradiction by A3,A5,A10,A12,AFF_1:30,def 1; end;
               o<>x proof assume o=x; then LIN a,o,c by A12,AFF_1:15;
             then c in A by A3,AFF_1:39;
             then c in A & c' in A by A3,A6,AFF_1:62;
             hence contradiction by A3,AFF_1:30; end;
            then b,x // b',c' by A2,A3,A5,A10,A12,A14,Def4;
            then b,x // b,c & LIN a,x,c by A3,A9,A12,AFF_1:14,15;
            then c in K by A12,A15,AFF_1:23;
           hence contradiction by A3,A4,A5,AFF_1:30;
          end;
        end;
       now assume A16: AP satisfies_DES_1; thus AP satisfies_DES
          proof let A,P,C,o,a,b,c,a',b',c';
           assume A17: o in A & o in P & o in C &
           o<>a & o<>b & o<>c & a in A & a' in A & b in P &
           b' in P & c in C & c' in C & A is_line & P is_line &
           C is_line & A<>P & A<>C & a,b // a',b' & a,c // a',c';
           assume A18: not b,c // b',c';
           then A19: b<>c & b'<>c' by AFF_1:12;
           A20: a<>b by A17,AFF_1:30;
           A21: a<>c by A17,AFF_1:30;
           A22: a'<>b' proof assume A23: a'=b';
            then a' in C & a',c' // c,a by A17,AFF_1:13,30;
             then a in C or a'=c' by A17,AFF_1:62;
            hence contradiction by A17,A18,A23,AFF_1:12,30; end;
           A24: a'<>c' proof assume a'=c';
            then a' in P & a',b' // b,a by A17,AFF_1:13,30;
            then a' in P & a in P by A17,A22,AFF_1:62;
            hence contradiction by A17,AFF_1:30; end;
           A25: not LIN a',b',c' proof assume LIN a',b',c';
            then a',b' // a',c' & LIN b',c',a' by AFF_1:15,def 1;
            then A26: a',b' // a,c & b',c' // b',a' by A17,A24,AFF_1:14,def 1;
            then a,b // a,c by A17,A22,AFF_1:14; then LIN a,b,c by AFF_1:def 1;
            then LIN b,c,a by AFF_1:15; then b,c // b,a by AFF_1:def 1;
            then b,c // a,b by AFF_1:13;
            then b,c // a',b' & b',c' // a',b' by A17,A20,A26,AFF_1:13,14;
            hence contradiction by A18,A22,AFF_1:14; end;
           A27: a<>a' proof assume a=a';
            then LIN a,b,b' & LIN a,c,c' by A17,AFF_1:def 1;
            then LIN b,b',a & LIN c,c',a by AFF_1:15;
            then (b=b' or a in P) & ( c =c' or a in C) by A17,AFF_1:39;
            hence contradiction by A17,A18,AFF_1:11,30; end;
           A28: o<>c' proof assume o=c';
            then c' in A & a',c' // a,c by A17,AFF_1:13;
            then c in A & c' in A by A17,A24,AFF_1:62;
           hence contradiction by A17,AFF_1:30; end;
           set K=Line(a',c'), M=Line(a,c), N=Line(b',c');
           A29: K is_line & M is_line & N is_line & a' in K &
            c' in K & a in M & c in M & b' in N & c' in N
              by A19,A21,A24,AFF_1:38; then consider D such that
           A30: b in D & N // D by AFF_1:63;
           A31: D is_line & D // N by A30,AFF_1:50;
             not M // D proof assume M // D; then M // N by A30,AFF_1:58;
            then a,c // b',c' by A29,AFF_1:53;
            then a',c' // b',c' by A17,A21,AFF_1:14; then c',a' // c',b'
             by AFF_1:13;
            then LIN c',a',b' by AFF_1:def 1;
            hence contradiction by A25,AFF_1:15; end; then consider x
           such that A32: x in M & x in D by A29,A31,AFF_1:72;
           A33: a,x // a',c' proof LIN a,c,x by A29,A32,AFF_1:33;
            then a,c // a,x by AFF_1:def 1; hence thesis by A17,A21,AFF_1:14;
end;
           A34: b,x // b',c' by A29,A30,A31,A32,AFF_1:53;
           A35: x<>c' proof assume x=c';
            then c',a // c',a' by A33,AFF_1:13; then LIN
 c',a,a' by AFF_1:def 1;
            then LIN a,a',c' by AFF_1:15; then c' in A by A17,A27,AFF_1:39;
            hence contradiction by A17,A28,AFF_1:30; end;
           A36: a<>x proof assume a=x; then a,b // b',c' by A29,A30,A31,A32,
AFF_1:53
;
            then a',b' // b',c' by A17,A20,AFF_1:14;
            then b',a' // b',c' by AFF_1:13; then LIN b',a',c' by AFF_1:def 1
;
            hence contradiction by A25,AFF_1:15; end;
           A37: not LIN a,b,x proof assume LIN a,b,x;
            then a,b // a,x by AFF_1:def 1; then a,b // a',c' by A33,A36,AFF_1:
14;
            then a',b' // a',c' by A17,A20,AFF_1:14;
            hence contradiction by A25,AFF_1:def 1; end;
           set T=Line(c',x);
           A38: T is_line & c' in T & x in T by A35,AFF_1:38;
:: stosujemy DES_1 dla trojkatow  abx  i  a'b'c'
           then o in T by A16,A17,A33,A34,A35,A37,Def5;
           then x in C by A17,A28,A38,AFF_1:30; then C=M by A17,A18,A29,A32,A34
,AFF_1:30;
           hence contradiction by A17,A29,AFF_1:30;
          end;
        end;
   hence thesis by A1;
  end;

theorem
Th17: AP satisfies_TDES implies AP satisfies_TDES_1
  proof assume A1: AP satisfies_TDES;
   thus AP satisfies_TDES_1
    proof let K,o,a,b,c,a',b',c';
      assume that A2: K is_line and A3: o in K & c in K & c' in K
      and A4: not a in K and A5: o<>c & a<>b & LIN o,a,a' &
      a,b // a',b' & b,c // b',c' & a,c // a',c' & a,b // K;
      assume A6: not LIN o,b,b'; A7: not b in K by A4,A5,AFF_1:49;
      A8: b<>c by A3,A4,A5,AFF_1:49;
      A9: o<>b & o<>a by A3,A4,A6,AFF_1:16; set A=Line(o,b), C=Line(o,a);
      A10: A is_line & C is_line & o in A & b in A
       & o in C & a in C by A9,AFF_1:26,def 3;
      then A11: a' in C by A3,A4,A5,AFF_1:39;
      consider P such that A12: a' in P & K // P by A2,AFF_1:63;
      A13: P is_line & P // K by A12,AFF_1:50;
        not A // P
        proof assume A // P; then A // K by A12,AFF_1:58;
         hence contradiction by A3,A7,A10,AFF_1:59;
        end;
       then consider x such that
       A14: x in A & x in P by A10,A13,AFF_1:72;
       A15: LIN o,b,x by A10,A14,AFF_1:33;
          a,b // a',x
         proof a',x // K by A12,A13,A14,AFF_1:54;
          hence thesis by A2,A5,AFF_1:45;
         end;
       then b,c // x,c' by A1,A2,A3,A4,A5,A15,Def7;
       then b',c' // x,c' by A5,A8,AFF_1:14; then c',b' // c',x by AFF_1:13;
       then LIN c',b',x by AFF_1:def 1; then A16: LIN b',x,c' by AFF_1:15;
         a,b // P by A5,A12,AFF_1:57; then a',b' // P by A5,AFF_1:46;
       then A17: b' in P by A12,A13,AFF_1:37;
      then LIN b',x,a' & LIN b',x,b' by A12,A13,A14,AFF_1:33;
      then LIN b',c',a' by A6,A15,A16,AFF_1:17; then b',c' // b',a' by AFF_1:
def 1;
      then A18: b',c' // a',b' by AFF_1:13;
      A19: b'<>c' proof assume A20: b'=c';
       then P=K by A3,A12,A17,AFF_1:59;
       then A21: a'=o by A2,A3,A4,A10,A11,A12,AFF_1:30;
         a',c' // c,a by A5,AFF_1:13;
       then b'=o by A2,A3,A4,A20,A21,AFF_1:62
; hence contradiction by A6,AFF_1:16; end;
      A22: a'<>b' proof assume A23: a'=b';
       then A24: a,c // b,c or a'=c' by A5,AFF_1:14;
         now assume a'=c';
        then b'=o by A2,A3,A4,A10,A11,A23,AFF_1:30
; hence contradiction by A6,AFF_1:16; end;
       then c,a // c,b by A24,AFF_1:13; then LIN c,a,b by AFF_1:def 1;
       then LIN a,c,b by AFF_1:15; then a,c // a,b by AFF_1:def 1;
       then a,b // a,c by AFF_1:13; then a,c // K by A5,AFF_1:46;
       then c,a // K by AFF_1:48;
       hence contradiction by A2,A3,A4,AFF_1:37; end;
        b,c // a',b' by A5,A18,A19,AFF_1:14;
      then a,b // b,c by A5,A22,AFF_1:14; then b,c // K by A5,AFF_1:46;
      then c,b // K by AFF_1:48; hence contradiction by A2,A3,A7,AFF_1:37;
     end;
    end;

theorem
   AP satisfies_TDES_1 implies AP satisfies_TDES_2
  proof assume A1: AP satisfies_TDES_1;
   thus AP satisfies_TDES_2
    proof let K,o,a,b,c,a',b',c';
     assume A2: K is_line & o in K & c in K & c' in K &
      not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' &
      b,c // b',c' & a,c // a',c' & a,b // K;
     assume A3: not a,b // a',b'; then A4: a'<>b' by AFF_1:12;
     A5: not b in K by A2,AFF_1:49;
     A6: o<>a & o<>b by A2,AFF_1:49; set A=Line(o,a), P=Line(o,b);
     A7: A is_line & P is_line & o in A & a in A &
      o in P & b in P by A6,AFF_1:38;
     then A8: a' in A & b' in P by A2,A6,AFF_1:39;
     A9: not b' in K proof assume A10: b' in K;
      then A11: b'=o by A2,A5,A7,A8,AFF_1:30;
A12:      b',c' // c,b by A2,AFF_1:13;
      then c' in A & a',c' // a,c by A2,A5,A7,A11,AFF_1:13,62;
      then a'=c' or c in A by A7,A8,AFF_1:62;
      hence contradiction by A2,A4,A5,A7,A10,A12,AFF_1:30,62; end;
 set T=Line(b',c');
     A13: T is_line & b' in T & c' in T by A2,A9,AFF_1:38;
     consider N such that A14: a' in N & K // N by A2,AFF_1:63;
     A15: N is_line & N // K by A14,AFF_1:50;
       not N // T proof assume N // T; then K // T by A14,AFF_1:58;
      hence contradiction by A2,A9,A13,AFF_1:59; end;
     then consider x such that
     A16: x in N & x in T by A13,A15,AFF_1:72;
       a',x // K by A14,A15,A16,AFF_1:54;
     then A17: a,b // a',x by A2,AFF_1:45;
        b,c // x,c' proof LIN c',b',x by A13,A16,AFF_1:33;
      then c',b' // c',x by AFF_1:def 1; then b',c' // x,c' by AFF_1:13;
      hence thesis by A2,A9,AFF_1:14; end;
      then LIN o,b,x by A1,A2,A17,Def8;
     then x in P by A6,A7,AFF_1:39;
     then P=T by A3,A7,A8,A13,A16,A17,AFF_1:30;
     then LIN c',b',b by A7,A13,AFF_1:33;
     then c',b' // c',b by AFF_1:def 1; then b',c' // b,c' by AFF_1:13;
     then b,c // b,c' by A2,A9,AFF_1:14; then LIN b,c,c' by AFF_1:def 1;
     then LIN c,c',b by AFF_1:15;
     then a,c // a',c & b,c // b',c by A2,A5,AFF_1:39;
     then c,a // c,a' & c,b // c,b' by AFF_1:13; then LIN c,a,a' &
     LIN c,b,b' by AFF_1:def 1; then LIN a,a',c & LIN b,b',c by AFF_1:15;
     then (a=a' or c in A) & (b=b' or c in P) by A7,A8,AFF_1:39;
     hence contradiction by A2,A3,A5,A7,AFF_1:11,30;
    end;
  end;

theorem
   AP satisfies_TDES_2 implies AP satisfies_TDES_3
 proof assume A1: AP satisfies_TDES_2;
  thus AP satisfies_TDES_3 proof let K,o,a,b,c,a',b',c';
  assume A2: K is_line & o in K & c in K & not a in K & o<>c & a<>b &
  LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' &
                                        b,c // b',c' & a,b // K;
  assume A3: not c' in K;
  A4: not b in K by A2,AFF_1:49;
  A5: o<>a & o<>b & a<>c & b<>c by A2,AFF_1:49;
  A6: not LIN a,b,c proof assume LIN a,b,c; then a,b // a,c by AFF_1:def 1;
   then a,c // K by A2,AFF_1:46; then c,a // K by AFF_1:48;
   hence contradiction by A2,AFF_1:37; end;
  set A=Line(o,a), P=Line(o,b), N=Line(b,c);
  A7: A is_line & P is_line & N is_line & o in A & a in A &
   o in P & b in P & b in N & c in N by A5,AFF_1:38;
  then A8: a' in A & b' in P by A2,A5,AFF_1:39;
  A9: A<>P proof assume A=P; then b in A & A // A by A7,AFF_1:55;
   then a,b // A by A7,AFF_1:54; then A // K by A2,AFF_1:67;
   hence contradiction by A2,A7,AFF_1:59; end;
  A10: a'<>b' proof assume A11: a'=b';
   then a,c // b,c or a'=c' by A2,AFF_1:14; then c,a // c,b or
   a'=c' by AFF_1:13; then LIN c,a,b or a'=c' by AFF_1:def 1;
   hence contradiction by A2,A3,A6,A7,A8,A9,A11,AFF_1:15,30; end;
  A12: a'<>c' proof assume a'=c'; then b,c // a',b' by A2,AFF_1:13;
   then a,b // b,c by A2,A10,AFF_1:14; then b,a // b,c by AFF_1:13;
   then LIN b,a,c by AFF_1:def 1; hence contradiction by A6,AFF_1:15; end;
    not a',c' // K proof assume a',c' // K; then a',c' // K &
   a',c' // a,c by A2,AFF_1:13; then a,c // K by A12,AFF_1:46;
   then c,a // K by AFF_1:48; hence contradiction by A2,AFF_1:37; end;
  then consider x such that A13: x in K & LIN a',c',x by A2,AFF_1:73;
  consider T such that A14: x in T & N // T by A7,AFF_1:63;
  A15: T is_line & T // N by A14,AFF_1:50;
    not T // P proof assume T // P; then N // P by A14,AFF_1:58;
   then c in P by A7,AFF_1:59;
   hence contradiction by A2,A4,A7,AFF_1:30; end; then consider
  y such that A16: y in T & y in P by A7,A15,AFF_1:72;
  A17: LIN o,b,y by A7,A16,AFF_1:33;
  A18: b,c // y,x by A7,A14,A16,AFF_1:53;
     a,c // a',x proof a',c' // a',x by A13,AFF_1:def 1;
   hence thesis by A2,A12,AFF_1:14; end;
   then a,b // a',y by A1,A2,A13,A17,A18,Def9;
  then a',b' // a',y by A2,AFF_1:14; then LIN a',b',y by AFF_1:def 1;
  then LIN b',y,a' & LIN b',y,b & LIN b',y,b'
                        by A7,A8,A16,AFF_1:15,33;
  then A19: b'=y or LIN b,b',a' by AFF_1:17;
A20:  now assume y=b';
   then b',c' // b',x by A2,A5,A18,AFF_1:14; then LIN b',c',x by AFF_1:def 1;
   then LIN c',x,b' & LIN c',x,a' & LIN c',x,c' by A13,AFF_1:15,16;
then LIN a',b',c' by A3,A13,AFF_1:17;
   then a',b' // a',c' by AFF_1:def 1; then a',b' // a,c by A2,A12,AFF_1:14;
   then a,b // a,c by A2,A10,AFF_1:14; hence contradiction by A6,AFF_1:def 1;
end;

    now assume A21: b=b';
   then b,a // b,a' by A2,AFF_1:13; then LIN b,a,a' by AFF_1:def 1;
   then LIN a,a',b by AFF_1:15; then a=a' or b in A by A7,A8,AFF_1:39;
then LIN a,c,c' & LIN b,c,c' by A2,A5,A7,A9,A21,AFF_1:30,def 1;
   then LIN c,c',a & LIN c,c',b & LIN c,c',c by AFF_1:15,16;
   hence contradiction by A2,A3,A6,AFF_1:17; end;
  then a' in P & a',b' // b,a by A2,A7,A8,A19,A20,AFF_1:13,39;
  then a in P by A7,A8,A10,AFF_1:62;
 hence contradiction by A2,A7,A9,AFF_1:30; end;
end;

theorem
   AP satisfies_TDES_3 implies AP satisfies_TDES
 proof assume A1: AP satisfies_TDES_3;
 thus AP satisfies_TDES proof let K,o,a,b,c,a',b',c';
 assume A2: K is_line & o in K & c in K & c' in K & not a in K &
 o<>c & a<>b & LIN o,a,a' & LIN
 o,b,b' & a,b // a',b' & a,c // a',c' & a,b // K;
 assume A3: not b,c // b',c'; then A4: b<>c & b'<>c' by AFF_1:12;
 A5: o<>a & o<>b & a<>c & b<>c by A2,AFF_1:49;
 A6: not LIN a,b,c proof assume LIN a,b,c; then a,b // a,c by AFF_1:def 1;
  then a,c // K by A2,AFF_1:46; then c,a // K by AFF_1:48;
  hence contradiction by A2,AFF_1:37; end;
 set A=Line(o,a), P=Line(o,b), M=Line(b,c), T=Line(a',c');
 A7: A is_line & P is_line & o in A & a in A & o in P & b in P
  by A5,AFF_1:38; then A8: a' in A & b' in P by A2,A5,AFF_1:39;
 A9: A<>P proof assume A=P; then b in A & A // A by A7,AFF_1:55;
  then a,b // A by A7,AFF_1:54; then A // K by A2,AFF_1:67;
  hence contradiction by A2,A7,AFF_1:59; end;
 A10: a'<>b' proof assume A11: a'=b';
  then a' in K &
  a',c' // c,a by A2,A7,A8,A9,AFF_1:13,30; then a'=c' by A2,AFF_1:62;
  hence contradiction by A3,A11,AFF_1:12; end;
 A12: a'<>c' proof assume a'=c'; then a' in P & a',b' // b,a
  by A2,A7,A8,AFF_1:13,30; then a in P by A7,A8,A10,AFF_1:62;
  hence contradiction by A2,A7,A9,AFF_1:30; end;
 then A13: M is_line & T is_line & b in M & c in M & a' in T &
  c' in T by A4,AFF_1:38; then consider N such that
 A14: b' in N & M // N by AFF_1:63;
 A15: N is_line & N // M by A14,AFF_1:50;
   not a',c' // N proof assume a',c' // N; then a',c' // N &
  a',c' // a,c by A2,AFF_1:13; then a,c // N by A12,AFF_1:46;
  then a,c // M by A14,AFF_1:57; then c,a // M by AFF_1:48;
  then a in M by A13,AFF_1:37; hence contradiction by A6,A13,AFF_1:33; end;
 then consider x such that A16: x in N & LIN a',c',x by A15,AFF_1:73;
 A17: x in T by A12,A13,A16,AFF_1:39;
 A18: b,c // b',x by A13,A14,A16,AFF_1:53;
    a,c // a',x proof a',c' // a',x by A16,AFF_1:def 1;
  hence thesis by A2,A12,AFF_1:14; end;
  then x in K by A1,A2,A18,Def10; then K=T by A2,A3,A13,A17,A18,AFF_1:30;
 then a' in P & a',b' // b,a
 by A2,A7,A8,A13,AFF_1:13,30; then a in P by A7,A8,A10,AFF_1:62;
 hence contradiction by A2,A7,A9,AFF_1:30; end;
end;

theorem
Th21: AP satisfies_des iff AP satisfies_des_1
  proof
    A1: now assume A2: AP satisfies_des;
     thus AP satisfies_des_1 proof let A,P,C,a,b,c,a',b',c';
     assume A3: A // P & a in A & a' in A & b in P &
     b' in P & c in C & c' in C & A is_line & P is_line &
     C is_line & A<>P & A<>C & a,b // a',b' & a,c // a',c' &
     b,c // b',c' & not LIN a,b,c & c <>c';
     assume A4: not A // C;
     A5: a<>b & a<>c & b<>c by A3,AFF_1:16;
     consider K such that A6: c' in K & A // K by A3,AFF_1:63;
     A7: K is_line & C<>K by A4,A6,AFF_1:50;
     A8: not a,c // K proof assume a,c // K;
      then a,c // A by A6,AFF_1:57; then A9: c in A by A3,AFF_1:37;
        a',c' // a,c by A3,AFF_1:13; then a',c' // A by A3,A5,A9,AFF_1:41;
      then c' in A by A3,AFF_1:37;
      hence contradiction by A3,A9,AFF_1:30; end; then consider x such that
     A10: x in K & LIN a,c,x by A7,AFF_1:73;
     A11: A<>K proof assume A=K;
      then a',c' // K & a',c' // a,c by A3,A6,AFF_1:13,54;
      then a'=c' by A8,AFF_1:46;
      then a',b' // a,b & a',b' // b,c by A3,AFF_1:13;
      then a'=b' or a,b // b,c by AFF_1:14;
      then b' in A or b,a // b,c by A3,AFF_1:13;
      then LIN b,a,c by A3,AFF_1:59,def 1;
      hence contradiction by A3,AFF_1:15; end;
       a,c // a,x by A10,AFF_1:def 1; then a,x // a',c' by A3,A5,AFF_1:14;
     then b,x // b',c' & b',c' // b,c by A2,A3,A6,A7,A10,A11,Def11,AFF_1:13;
     then A12: b,x // b,c or b'=c' by AFF_1:14;
       now assume b'=c';
      then a,b // a,c or a'=b' by A3,AFF_1:14;
      hence contradiction by A3,AFF_1:59,def 1; end;
     then LIN b,x,c by A12,AFF_1:def 1; then LIN x,c,b & LIN x,c,a & LIN x,c,
c
     by A10,AFF_1:15,16; then c in K by A3,A10,AFF_1:17;
     hence contradiction by A3,A6,A7,AFF_1:30; end;
    end;
       now assume A13: AP satisfies_des_1; thus AP satisfies_des proof
     let A,P,C,a,b,c,a',b',c'; assume A14: A // P & A // C & a in A &
     a' in A & b in P & b' in P & c in C & c' in C & A is_line &
     P is_line & C is_line & A<>P & A<>C & a,b // a',b' & a,c // a',c';
      assume A15: not b,c // b',c'; then A16: b<>c & b'<>c' by AFF_1:12;
     A17: a<>c & a<>b & a'<>b' & a'<>c' by A14,AFF_1:59;
     set K=Line(a,c), N=Line(b',c');
     A18: P // C by A14,AFF_1:58; A19: K is_line & N is_line &
      a in K & c in K & b' in N & c' in N by A16,A17,AFF_1:38;
     then consider M such that A20: b in M & N // M by AFF_1:63;
     A21: M is_line by A20,AFF_1:50;
     A22: not LIN a,b,c proof assume A23: LIN a,b,c; then LIN
 b,c,a by AFF_1:15;
      then b,c // b,a by AFF_1:def 1; then b,c // a,b by AFF_1:13;
      then A24: b,c // a',b' by A14,A17,AFF_1:14; LIN c,b,a by A23,AFF_1:15;
      then c,b // c,a by AFF_1:def 1; then b,c // a,c by AFF_1:13;
      then b,c // a',c' by A14,A17,AFF_1:14;
      then a',c' // a',b' by A16,A24,AFF_1:14;
      then LIN a',c',b' by AFF_1:def 1; then LIN b',c',a' by AFF_1:15;
      then b',c' // b',a' by AFF_1:def 1; then b',c' // a',b' by AFF_1:13;
      hence contradiction by A15,A17,A24,AFF_1:14; end;
     A25: not LIN a',b',c' proof assume LIN a',b',c';
     then a',b' // a',c' by AFF_1:def 1; then a,b // a',c' by A14,A17,AFF_1:14;
     then a,b // a,c by A14,A17,AFF_1:14;
     hence contradiction by A22,AFF_1:def 1; end;
     A26: not K // M proof assume K // M; then K // N by A20,AFF_1:58
; then a,c // b',c' by A19,AFF_1:53; then a',c' // b',c' by A14,A17,AFF_1:14;
      then c',a' // c',b' by AFF_1:13; then LIN c',a',b' by AFF_1:def 1;
      hence contradiction by A25,AFF_1:15; end;
     then consider x such that A27: x in K & x in M by A19,A21,AFF_1:72; A28:
b',c' // b,x by A19,A20,A27,AFF_1:53;
     then A29: b,x // b',c' by AFF_1:13;
     A30: a,x // a',c' proof LIN a,c,x by A19,A27,AFF_1:33;
      then a,c // a,x by AFF_1:def 1;
      hence a,x // a',c' by A14,A17,AFF_1:14; end;
     set D=Line(x,c'); A31: x in D & c' in D by AFF_1:26;
     A32: x<>c' proof assume x=c';
      then M=N by A19,A20,A27,AFF_1:59;
      then A33: P=N or b=b' by A14,A19,A20,AFF_1:30;
A34:      now assume P=N; then c' in P & c in P & P // P by A14,A18,A19,AFF_1:
59;
       hence contradiction by A14,A15,AFF_1:53; end;

      then b,a // b,a' by A14,A33,AFF_1:13; then LIN b,a,a' by AFF_1:def 1;
      then LIN a,a',b by AFF_1:15; then b in A or a=a' by A14,AFF_1:39;
      then LIN a',c,c' by A14,AFF_1:59,def 1; then LIN
 c,c',a' by AFF_1:15;
      then c =c' or a' in C by A14,AFF_1:39;
      hence contradiction by A14,A15,A33,A34,AFF_1:11,59
; end; then A35: D is_line by AFF_1:38;
     A36: not LIN a,b,x proof assume LIN a,b,x; then LIN x,b,a by AFF_1:15;
      then x,b // x,a by AFF_1:def 1; then A37: x,a // x,b by AFF_1:13;
      A38: x<>b by A19,A22,A27,AFF_1:33;
        a<>x proof assume a=x;
       then a,b // b',c' by A28,AFF_1:13
; then a',b' // b',c' by A14,A17,AFF_1:14;
       then b',a' // b',c' by AFF_1:13; then LIN b',a',c' by AFF_1:def 1;
       hence contradiction by A25,AFF_1:15; end;
      hence contradiction by A19,A20,A21,A26,A27,A37,A38,AFF_1:52; end;
        A<>D proof assume A=D; then c' in A by AFF_1:26;
      hence contradiction by A14,AFF_1:59; end;
     then A // D by A13,A14,A29,A30,A31,A32,A35,A36,Def12; then D // C by A14,
AFF_1:58;
     then C=D by A14,A31,AFF_1:59;
     then C=K by A14,A15,A19,A27,A29,A31,AFF_1:30;
     hence contradiction by A14,A19,AFF_1:59; end;
    end;
   hence thesis by A1;
  end;

theorem
   AP satisfies_pap iff AP satisfies_pap_1
  proof
   A1: now assume A2: AP satisfies_pap;
        thus AP satisfies_pap_1
         proof let M,N,a,b,c,a',b',c';
          assume A3: M is_line & N is_line & a in M &
           b in M & c in M & M // N & M<>N & a' in N &
           b' in N & a,b' // b,a' & b,c' // c,b' &
           a,c' // c,a' & a'<>b';
          assume A4: not c' in N;
          A5: c <>b' by A3,AFF_1:59;
          A6: c <>a' by A3,AFF_1:59;
          A7: a<>b proof assume a=b;
           then LIN a,b',a' by A3,AFF_1:def 1; then LIN a',b',a by AFF_1:15;
           then a'=b' or a in N by A3,AFF_1:39;
           hence contradiction by A3,AFF_1:59; end;
          set C=Line(c,b');
          A8: C is_line & c in C & b' in C by A5,AFF_1:38;
          then consider K such that A9: b in K & C // K by AFF_1:63;
          A10: K is_line & K // C by A9,AFF_1:50;
            not K // N proof assume K // N; then C // N & N // M
           by A3,A9,AFF_1:58; then C // M by AFF_1:58;
           then b' in M by A3,A8,AFF_1:59;
           hence contradiction by A3,AFF_1:59; end; then consider
          x such that A11: x in K & x in N by A3,A10,AFF_1:72;
          A12: c'<>b proof assume c'=b;
           then a' in M by A3,A7,AFF_1:62;
           hence contradiction by A3,AFF_1:59; end;
          A13: b,x // c,b' by A8,A9,A10,A11,AFF_1:53;
           then a,x // c,a' by A2,A3,A11,Def13;
          then a,x // a,c' by A3,A6,AFF_1:14;
          then A14: LIN
 a,x,c' by AFF_1:def 1; b,x // b,c' by A3,A5,A13,AFF_1:14;
          then LIN b,x,c' by AFF_1:def 1;
          then LIN c',x,a & LIN c',x,b & LIN c',x,c' by A14,AFF_1:15,16;
          then LIN a,b,c' by A4,A11,AFF_1:17; then c' in M by A3,A7,AFF_1:39;
          then b' in M by A3,A12,AFF_1:62;
         hence contradiction by A3,AFF_1:59; end;
       end;
      now assume A15: AP satisfies_pap_1;
        thus AP satisfies_pap
         proof let M,N,a,b,c,a',b',c';
          assume A16: M is_line & N is_line & a in M &
          b in M & c in M & M // N & M<>N & a' in N & b' in N &
          c' in N & a,b' // b,a' & b,c' // c,b';
          assume A17: not a,c' // c,a';
          then A18: a<>c' & c <>a' by AFF_1:12;
          set A=Line(c,a'), C=Line(c,b'), D=Line(b,c');
          A19: c <>b' & b<>c' by A16,AFF_1:59;
          A20: a'<>b' proof assume A21: a'=b'; then a',a // a',b by A16,AFF_1:
13
;
           then LIN a',a,b by AFF_1:def 1; then LIN a,b,a' by AFF_1:15;
           then a=b or a' in M by A16,AFF_1:39;
           hence contradiction by A16,A17,A21,AFF_1:59; end;
          A22: A is_line & C is_line & D is_line & c in A &
           a' in A & c in C & b' in C & b in D & c' in D
                                            by A18,A19,AFF_1:38;
          then consider P such that A23: a in P & A // P by AFF_1:63;
          A24: P is_line & P // A by A23,AFF_1:50;
            not D // P proof assume D // P;
           then b,c' // P by A22,AFF_1:54;
           then c,b' // P by A16,A19,AFF_1:46; then c,b' // A by A23,AFF_1:57
;
           then b' in A by A22,AFF_1:37;
           then c in N by A16,A20,A22,AFF_1:30; hence contradiction by A16,
AFF_1:59; end;
          then consider x such that
          A25: x in D & x in P by A22,A24,AFF_1:72;
          A26: a,x // c,a' by A22,A23,A24,A25,AFF_1:53;
             b,x // c,b' proof LIN b,x,c' by A22,A25,AFF_1:33;
           then b,x // b,c' by AFF_1:def 1; hence thesis by A16,A19,AFF_1:14;
end;
          then x in N by A15,A16,A20,A26,Def14;
          then x=c' or b in N by A16,A22,A25,AFF_1:30;
          hence contradiction by A16,A17,A22,A23,A24,A25,AFF_1:53,59;
         end;
       end;
  hence thesis by A1;
  end;

theorem
Th23: AP satisfies_PAP implies AP satisfies_pap
  proof assume A1: AP satisfies_PAP;
   thus AP satisfies_pap
    proof let M,N,a,b,c,a',b',c';
     assume A2: M is_line & N is_line & a in M &
     b in M & c in M & M // N & M<>N & a' in N &
     b' in N & c' in N & a,b' // b,a' & b,c' // c,b';
     assume A3: not a,c' // c,a';
     A4: a<>b' & c <>b' & b<>c' & b<>a' & a<>c' by A2,AFF_1:59;
     A5: a<>b & a<>c & b<>c proof
      A6: now assume A7: a=b;
       then LIN a,b',a' by A2,AFF_1:def 1; then LIN a',b',a by AFF_1:15;
       then a'=b' or a in N by A2,AFF_1:39;
       hence contradiction by A2,A3,A7,AFF_1:59; end;
      A8: now assume A9: a=c;
       then b,c' // b,a' by A2,A4,AFF_1:14; then LIN b,c',a' by AFF_1:def 1;
       then LIN a',c',b by AFF_1:15; then a'=c' or b in N by A2,AFF_1:39;
hence
         contradiction by A2,A3,A9,AFF_1:11,59; end;
        now assume A10: b=c;
       then LIN b,c',b' by A2,AFF_1:def 1; then LIN b',c',b by AFF_1:15;
       then b'=c' or b in N by A2,AFF_1:39;
       hence contradiction by A2,A3,A10,AFF_1:59; end;
      hence thesis by A6,A8; end;
      A11: a'<>b' & a'<>c' & b'<>c' proof
       A12: now assume a'=b';
        then a',a // a',b by A2,AFF_1:13; then LIN a',a,b by AFF_1:def 1;
        then LIN a,b,a' by AFF_1:15; then a' in M by A2,A5,AFF_1:39;
        hence contradiction by A2,AFF_1:59; end;
       A13: now assume a'=c';
        then a,b' // c,b' by A2,A4,AFF_1:14; then b',a // b',c by AFF_1:13;
        then LIN b',a,c by AFF_1:def 1; then LIN a,c,b' by AFF_1:15;
        then b' in M by A2,A5,AFF_1:39;
        hence contradiction by A2,AFF_1:59; end;
         now assume b'=c';
        then b',b // b',c by A2,AFF_1:13; then LIN b',b,c by AFF_1:def 1;
        then LIN b,c,b' by AFF_1:15; then b' in M by A2,A5,AFF_1:39;
        hence contradiction by A2,AFF_1:59; end;
        hence thesis by A12,A13; end;
      set K=Line(a,c'), C=Line(c,b');
      A14: K is_line & C is_line & a in K & c' in K &
       c in C & b' in C by A4,AFF_1:38; then consider T
      such that A15: a' in T & K // T by AFF_1:63;
      A16: T is_line & T // K by A15,AFF_1:50;
        not C // T proof assume C // T; then C // K by A15,AFF_1:58;
       then c,b' // a,c' by A14,AFF_1:53;
       then b,c' // a,c' by A2,A4,AFF_1:14; then c',b // c',a by AFF_1:13;
       then LIN c',b,a by AFF_1:def 1; then LIN a,b,c' by AFF_1:15;
       then c' in M by A2,A5,AFF_1:39;
       hence contradiction by A2,AFF_1:59; end;
      then consider x such that A17: x in C & x in T by A14,A16,AFF_1:72;
      A18: a,c' // x,a' by A14,A15,A17,AFF_1:53;
      A19: x<>b proof assume x=b; then LIN b,c,b' by A14,A17,AFF_1:33;
       then b' in M by A2,A5,AFF_1:39;
       hence contradiction by A2,AFF_1:59; end;
 set D=Line(x,b);
      A20: D is_line & x in D & b in D by A19,AFF_1:38;
        not D // N proof assume D // N; then D // M by A2,AFF_1:58;
then x in M by A2,A20,AFF_1:59;
       then c in T or b' in M by A2,A14,A17,AFF_1:30;
       hence contradiction by A2,A3,A14,A15,AFF_1:53,59; end;
      then consider o such that A21: o in D & o in N by A2,A20,AFF_1:72;
      A22: b,c' // x,b' proof LIN b',c,x by A14,A17,AFF_1:33;
       then b',c // b',x by AFF_1:def 1; then c,b' // x,b' by AFF_1:13;
       hence b,c' // x,b' by A2,A4,AFF_1:14; end;
      A23: a'<>x proof assume a'=x;
       then c,b' // a',b' by A2,A4,A22,AFF_1:14; then b',a' // b',c
       by AFF_1:13;
       then LIN b',a',c by AFF_1:def 1; then c in N by A2,A11,AFF_1:39;
       hence contradiction by A2,AFF_1:59; end;
      A24: b'<>x proof assume b'=x;
       then a,c' // a',b' by A14,A15,A17,AFF_1:53;
       then a,c' // N by A2,A11,AFF_1:41;
       then c',a // N by AFF_1:48; then a in N by A2,AFF_1:37;
       hence contradiction by A2,AFF_1:59; end;
        not a,b' // D proof assume a,b' // D;
       then b,a' // D by A2,A4,AFF_1:46; then a' in D by A20,AFF_1:37;
       then b in T by A15,A16,A17,A20,A23,AFF_1:30;
       then b,a' // a,c' by A14,A15,A16,AFF_1:53;
       then a,b' // a,c' by A2,A4,AFF_1:14; then LIN a,b',c' by AFF_1:def 1;
       then LIN b',c',a by AFF_1:15; then a in N by A2,A11,AFF_1:39;
       hence contradiction by A2,AFF_1:59; end;
      then consider y such that A25: y in D & LIN a,b',y by A20,AFF_1:73;
      A26: y,b' // b,a' proof LIN b',a,y by A25,AFF_1:15;
       then b',a // b',y by AFF_1:def 1; then a,b' // y,b' by AFF_1:13; hence
         y,b' // b,a' by A2,A4,AFF_1:14; end;
      A27: D<>N by A2,A20,AFF_1:59;
      A28: o<>b' & o<>c' & o<>a' proof
       A29: now assume o=b';
        then LIN b',x,b by A20,A21,AFF_1:33; then b',x // b',b by AFF_1:def 1
;
        then x,b' // b,b' by AFF_1:13; then b,c' // b,b' by A22,A24,AFF_1:14;
        then LIN b,c',b' by AFF_1:def 1; then LIN b',c',b by AFF_1:15;
        then b in N by A2,A11,AFF_1:39;
        hence contradiction by A2,AFF_1:59; end;
       A30: now assume o=a';
        then LIN a',b,x by A20,A21,AFF_1:33; then a',b // a',x by AFF_1:def 1
;
        then b,a' // x,a' by AFF_1:13; then a,b' // x,a' by A2,A4,AFF_1:14;
        then a,b' // a,c' by A18,A23,AFF_1:14; then LIN a,b',c' by AFF_1:def 1;
        then LIN b',c',a by AFF_1:15; then a in N by A2,A11,AFF_1:39;
        hence contradiction by A2,AFF_1:59; end;
         now assume o=c';
        then D // C by A2,A4,A14,A20,A21,AFF_1:52;
        then b in C by A17,A20,AFF_1:59; then LIN c,b,b' by A14,AFF_1:33;
        then b' in M by A2,A5,AFF_1:39;
        hence contradiction by A2,AFF_1:59; end;
        hence thesis by A29,A30; end;
         o<>b & o<>x & o<>y proof
       A31: now assume o=x;
        then N=T by A2,A15,A16,A17,A21,A23,AFF_1:30;
        then N=K by A2,A14,A15,AFF_1:59;
        hence contradiction by A2,A14,AFF_1:59; end;
         now assume o=y; then LIN b',o,a & LIN b',o,a' & LIN b',o,b'
                            by A2,A21,A25,AFF_1:15,33;
        then LIN a',b',a by A28,AFF_1:17;
        then a in N by A2,A11,AFF_1:39;
       hence contradiction by A2,AFF_1:59; end;
       hence thesis by A2,A21,A31,AFF_1:59; end;
      then y,c' // x,a' by A1,A2,A20,A21,A22,A25,A26,A27,A28,Def2;
      then y,c' // a,c' by A18,A23,AFF_1:14; then c',y // c',a by AFF_1:13;
      then LIN c',y,a by AFF_1:def 1;
      then LIN a,y,c' & LIN a,y,b' & LIN a,y,a by A25,AFF_1:15,16;
      then a=y or LIN b',c',a by AFF_1:17;
      then a in D or a in
 N by A2,A11,A25,AFF_1:39; then D // N by A2,A5,A20,AFF_1:30,59;
     hence contradiction by A21,A27,AFF_1:59;
    end;
  end;

theorem
Th24: AP satisfies_PPAP iff AP satisfies_PAP & AP satisfies_pap
 proof
  A1: AP satisfies_PPAP implies AP satisfies_PAP & AP satisfies_pap proof
   assume A2: AP satisfies_PPAP; thus AP satisfies_PAP
    proof let M,N,o,a,b,c,a',b',c';
    assume M is_line & N is_line & M<>N & o in M & o in N &
   o<>a & o<>a' & o<>b & o<>b' & o<>c & o<>c' & a in M &
   b in M & c in M & a' in N & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b'; hence thesis by A2,Def1; end;
                    thus AP satisfies_pap proof let M,N,a,b,c,a',b',c';
    assume M is_line & N is_line & a in M & b in M & c in M &
     M // N & M<>N & a' in N & b' in N & c' in N &
      a,b' // b,a' & b,c' // c,b'; hence thesis by A2,Def1; end;
   end;
     AP satisfies_PAP & AP satisfies_pap implies AP satisfies_PPAP
   proof assume A3: AP satisfies_PAP & AP satisfies_pap;
   thus AP satisfies_PPAP proof let M,N,a,b,c,a',b',c';
   assume A4: M is_line & N is_line & a in M &
   b in M & c in M & a' in N & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b';

      now assume A5: M<>N; assume A6: not thesis;
       now assume not M // N; then consider o such that
     A7: o in M & o in N by A4,AFF_1:72;
     A8: o<>a proof assume A9: o=a; then o,b' // a',b by A4,AFF_1:13;
      then o=b' or b in N by A4,A7,AFF_1:62;
      then o=b' or o=b by A4,A5,A7,AFF_1:30; then c,o // b,c' or
      o,c' // b',c by A4,AFF_1:13; then c' in M or c =o or
      c in N or o=c' by A4,A7,AFF_1:62;
      then o=c or o=c' by A4,A5,A7,AFF_1:30;
      hence contradiction by A4,A6,A7,A9,AFF_1:12,65; end;
     A10: o<>b proof assume A11: o=b; then o,a' // b',a by A4,AFF_1:13;
      then A12: o=a' or a in N by A4,A7,AFF_1:62;

        o,c' // b',c by A4,A11,AFF_1:13; then o=c' or
      c in N by A4,A7,AFF_1:62; then o=c' or
      o=c by A4,A5,A7,AFF_1:30;
      hence contradiction by A4,A5,A6,A7,A8,A12,AFF_1:12,30,65; end;
     A13: o<>c proof assume A14: o=c; then o,b' // c',b by A4,AFF_1:13;
      then o=b' or b in N by A4,A7,AFF_1:62;
      then a' in M by A4,A7,A8,A10,AFF_1:30,62;
      then a'=o by A4,A5,A7,AFF_1:30;
      hence contradiction by A6,A14,AFF_1:12; end;
     A15: o<>a' proof assume A16: o=a'; then o,b // a,b' by A4,AFF_1:13;
      then b' in M by A4,A7,A10,AFF_1:62;
      then o=b' by A4,A5,A7,AFF_1:30; then c,o // b,c' by A4,AFF_1:13;
      then a' in M & c' in M by A4,A7,A13,A16,AFF_1:62;
      hence contradiction by A4,A6,AFF_1:65; end;
     A17: o<>b' proof assume A18: o=b';


      then o,c // b,c' by A4,AFF_1:13;
      then a' in M & c' in M by A4,A7,A8,A13,A18,AFF_1:62;
      hence contradiction by A4,A6,AFF_1:65; end;
        o<>c' proof assume A19: o=c';
      then b' in M by A4,A7,A10,AFF_1:62; then a,o // b,a' by A4,A5,A7,AFF_1:30
;
      then a' in M & c' in M by A4,A7,A8,A19,AFF_1:62;
      hence contradiction by A4,A6,AFF_1:65; end;
     hence thesis by A3,A4,A5,A7,A8,A10,A13,A15,A17,Def2; end;
    hence thesis by A3,A4,A5,Def13; end;
   hence thesis by A4,AFF_1:65; end; end;
 hence thesis by A1; end;

theorem
   AP satisfies_PAP implies AP satisfies_DES
 proof assume A1: AP satisfies_PAP; then AP satisfies_pap by Th23;
  then A2: AP satisfies_PPAP by A1,Th24;
  thus AP satisfies_DES
   proof let A,P,C,o,a,b,c,a',b',c';
    assume A3: o in A & o in P & o in C & o<>a & o<>b & o<>c &
     a in A & a' in A & b in P & b' in P & c in C & c' in C &
     A is_line & P is_line & C is_line & A<>P & A<>C &
     a,b // a',b' & a,c // a',c';
    assume A4: not b,c // b',c';
    then A5: b<>c & b'<>c' by AFF_1:12;
    A6: a<>b & a<>c by A3,AFF_1:30;
    A7: a<>a' proof assume a=a';
     then LIN a,b,b' & LIN a,c,c' by A3,AFF_1:def 1;
     then LIN b,b',a & LIN c,c',a by AFF_1:15;
     then (b=b' or a in P) & (c =c' or a in C) by A3,AFF_1:39;
     hence contradiction by A3,A4,AFF_1:11,30; end;
    A8: a'<>b' proof assume A9: a'=b';
     then a' in C & a',c' // c,a by A3,AFF_1:13,30;
       then a in C or a'=c' by A3,AFF_1:62;
      hence contradiction by A3,A4,A9,AFF_1:12,30; end;
    A10: a'<>c' proof assume a'=c';
     then a' in P & a',b' // b,a by A3,AFF_1:13,30;
     then a' in P & a in P by A3,A8,AFF_1:62;
     hence contradiction by A3,AFF_1:30; end;
    A11: not LIN a',b',c' proof assume LIN a',b',c';
     then a',b' // a',c' & LIN b',c',a' by AFF_1:15,def 1;
     then A12: a',b' // a,c & b',c' // b',a' by A3,A10,AFF_1:14,def 1;
     then a,b // a,c by A3,A8,AFF_1:14; then LIN a,b,c by AFF_1:def 1;
     then LIN b,c,a by AFF_1:15; then b,c // b,a by AFF_1:def 1;
     then b,c // a,b by AFF_1:13;
     then b,c // a',b' & b',c' // a',b' by A3,A6,A12,AFF_1:13,14;
     hence contradiction by A4,A8,AFF_1:14; end;
    A13: not LIN a,b,c proof assume LIN a,b,c; then a,b // a,c by AFF_1:def 1
;
     then a,b // a',c' by A3,A6,AFF_1:14;
     then a',b' // a',c' by A3,A6,AFF_1:14;
     hence contradiction by A11,AFF_1:def 1; end;
    A14: not b in C proof assume b in C; then b in C & b' in C by A3,AFF_1:30
;
      hence contradiction by A3,A4,AFF_1:65; end;
    A15: o<>a' proof assume o=a'; then a' in P &
     a',b' // b,a by A3,AFF_1:13; then a in P & a' in P
     by A3,A8,AFF_1:62; hence contradiction by A3,AFF_1:30; end;
    A16: o<>b' proof assume o=b'; then b' in A & b',a' // a,b
     by A3,AFF_1:13; then b in A & b' in A by A3,A8,AFF_1:62;
     hence contradiction by A3,AFF_1:30; end;
     now assume A17: not b,c // A;
    set M=Line(b,c), N=Line(a,b), D=Line(a,c);
    A18: M is_line & N is_line & b in M & D is_line & c in M
     & a in N & b in N & a in D & c in D by A5,A6,AFF_1:38;
    then consider K such that A19: o in K & M // K by AFF_1:63;
    A20: K is_line & K // M by A19,AFF_1:50;
       not N // K proof assume N // K; then N // M by A19,AFF_1:58;
     then c in N by A18,AFF_1:59;
     hence contradiction by A13,A18,AFF_1:33; end;
    then consider p such that A21: p in N & p in K by A18,A20,AFF_1:72;
    consider T such that A22: p in T & D // T by A18,AFF_1:63;
    A23: T is_line & T // D by A22,AFF_1:50;
      not C // T proof assume C // T; then C // D by A22,AFF_1:58;
     then a in C by A3,A18,AFF_1:59;
     hence contradiction by A3,AFF_1:30; end; then consider q
    such that A24: q in C & q in T by A3,A23,AFF_1:72;
    A25: o<>p proof assume o=p;
     then LIN o,a,b & LIN o,a,a' & LIN o,a,a by A3,A18,A21,AFF_1:33;
     then b in A by A3,AFF_1:39;
     hence contradiction by A3,AFF_1:30; end;
   A26: b,c // p,o & p,q // a,c by A18,A19,A21,A22,A23,A24,AFF_1:53;
   then A27: b,q // a,o by A2,A3,A18,A21,A24,Def1;
   A28: p<>a' proof assume p=a';
    then b in A by A3,A7,A18,A21,AFF_1:30; hence contradiction by A3,AFF_1:30
; end;
   A29: K<>A by A17,A18,A19,AFF_1:54;
   set R=Line(a',p);
   A30: R is_line & a' in R & p in R by A28,AFF_1:38;
     not b,q // R proof assume b,q // R;
    then a,o // R & A // A by A3,A14,A24,A27,AFF_1:46,55;
    then a,o // R & a,o // A by A3,AFF_1:54;
    then R // A by A3,AFF_1:67;
    then p in A by A3,A30,AFF_1:59; hence contradiction
    by A3,A19,A20,A21,A25,A29,AFF_1:30; end; then consider r
   such that A31: r in R & LIN b,q,r by A30,AFF_1:73;
   A32: p,q // a',c' by A3,A6,A26,AFF_1:14;
   A33: a',o // r,q proof LIN q,r,b by A31,AFF_1:15;
    then q,r // q,b by AFF_1:def 1; then r,q // b,q by AFF_1:13;
    then A34: r,q // a,o by A14,A24,A27,AFF_1:14; LIN o,a,a' by A3,AFF_1:33;
    then o,a // o,a' by AFF_1:def 1; then a',o // a,o by AFF_1:13;
    hence thesis by A3,A34,AFF_1:14; end;
   then A35: p,o // r,c' by A2,A3,A24,A30,A31,A32,Def1;
   then A36: b,c // r,c' by A25,A26,AFF_1:14;
   A37: p,b // a',b' proof LIN b,a,p by A18,A21,AFF_1:33;
    then b,a // b,p by AFF_1:def 1; then a,b // p,b by AFF_1:13;
    hence thesis by A3,A6,AFF_1:14; end;
      a',o // r,b proof LIN r,b,q by A31,AFF_1:15;
then A38:    r,b // r,q by AFF_1:def 1;
      now assume r=q; then b,r // a,o & LIN o,a,a' by A2,A3,A18,A21,A24,A26,
Def1,AFF_1:33;
     then r,b // o,a & o,a // o,a' by AFF_1:13,def 1;
     hence r,b // o,a' by A3,AFF_1:14; end;
    hence thesis by A33,A38,AFF_1:13,14; end;
   then A39: p,o // r,b' by A2,A3,A30,A31,A37,Def1;
   then r,c' // r,b' by A25,A35,AFF_1:14; then LIN r,c',b' by AFF_1:def 1;
   then LIN c',b',r by AFF_1:15; then c',b' // c',r by AFF_1:def 1;
   then r,c' // b',c' by AFF_1:13; then r=c' by A4,A36,AFF_1:14;
   then p,o // b',c' by A39,AFF_1:13;
   hence contradiction by A4,A25,A26,AFF_1:14; end;
  then A40: not b',c' // A by A3,A4,AFF_1:45;
      set M=Line(b',c'), N=Line(a',b'), D=Line(a',c');
    A41: M is_line & N is_line & b' in M & D is_line & c' in M
     & a' in N & b' in N & a' in D & c' in D by A5,A8,A10,AFF_1:38;
    then consider K such that A42: o in K & M // K by AFF_1:63;
    A43: K is_line & K // M by A42,AFF_1:50;
       not N // K proof assume N // K; then N // M by A42,AFF_1:58;
     then c' in N by A41,AFF_1:59;
     hence contradiction by A11,A41,AFF_1:33; end;
    then consider p such that A44: p in N & p in K by A41,A43,AFF_1:72;
    consider T such that A45: p in T & D // T by A41,AFF_1:63;
    A46: T is_line & T // D by A45,AFF_1:50;
      not C // T proof assume C // T; then C // D by A45,AFF_1:58;
     then a' in C by A3,A41,AFF_1:59;
     hence contradiction by A3,A15,AFF_1:30; end; then consider q
    such that A47: q in C & q in T by A3,A46,AFF_1:72;
    A48: o<>p proof assume o=p;
     then LIN o,a',b' & LIN o,a',a & LIN o,a',a' by A3,A41,A44,AFF_1:33;
     then b' in A &
     a',b' // a,b by A3,A15,AFF_1:13,39; then b in A & b' in A
     by A3,A8,AFF_1:62; hence contradiction by A3,AFF_1:30; end;
   A49: b',c' // p,o & p,q // a',c' by A41,A42,A44,A45,A46,A47,AFF_1:53;
   then A50: b',q // a',o by A2,A3,A41,A44,A47,Def1;
   A51: p<>a proof assume p=a;
    then b' in A by A3,A7,A41,A44,AFF_1:30
; hence contradiction by A3,A16,AFF_1:30; end;
   A52: K<>A by A40,A41,A42,AFF_1:54;
   A53: b'<>q proof assume b'=q;
    then P=C by A3,A16,A47,AFF_1:30;
    hence contradiction by A3,A4,AFF_1:65; end;
   set R=Line(a,p);
   A54: R is_line & a in R & p in R by A51,AFF_1:38;
     not b',q // R proof assume b',q // R;
    then a',o // R & A // A by A3,A50,A53,AFF_1:46,55;
    then a',o // R & a',o // A by A3,AFF_1:54;
    then R // A by A15,AFF_1:67;
    then p in A by A3,A54,AFF_1:59; hence contradiction
    by A3,A42,A43,A44,A48,A52,AFF_1:30; end; then consider r
   such that A55: r in R & LIN b',q,r by A54,AFF_1:73;
   A56: p,q // a,c by A3,A10,A49,AFF_1:14;
   A57: a,o // r,q proof LIN q,r,b' by A55,AFF_1:15;
    then q,r // q,b' by AFF_1:def 1; then r,q // b',q by AFF_1:13;
    then A58: r,q // a',o by A50,A53,AFF_1:14; LIN o,a,a' by A3,AFF_1:33;
    then o,a // o,a' by AFF_1:def 1; then a,o // a',o by AFF_1:13;
    hence thesis by A15,A58,AFF_1:14; end;
   then A59: p,o // r,c by A2,A3,A47,A54,A55,A56,Def1;
   then A60: b',c' // r,c by A48,A49,AFF_1:14;
   A61: p,b' // a,b proof LIN b',a',p by A41,A44,AFF_1:33;
    then b',a' // b',p by AFF_1:def 1; then p,b' // a',b' by AFF_1:13;
    hence thesis by A3,A8,AFF_1:14; end;
      a,o // r,b' proof LIN r,b',q by A55,AFF_1:15;
then A62:    r,b' // r,q by AFF_1:def 1;
      now assume r=q; then b',r // a',o & LIN
 o,a',a by A2,A3,A41,A44,A47,A49,Def1,AFF_1:33;
     then r,b' // o,a' & o,a' // o,a by AFF_1:13,def 1;
     hence r,b' // o,a by A15,AFF_1:14; end;
    hence thesis by A57,A62,AFF_1:13,14; end;
   then A63: p,o // r,b by A2,A3,A54,A55,A61,Def1;
   then r,c // r,b by A48,A59,AFF_1:14; then LIN r,c,b by AFF_1:def 1;
   then LIN c,b,r by AFF_1:15; then c,b // c,r by AFF_1:def 1;
   then b,c // r,c by AFF_1:13; then r=c by A4,A60,AFF_1:14;
   then b,c // p,o by A63,AFF_1:13;
   hence contradiction by A4,A48,A49,AFF_1:14;
  end;
 end;

theorem
   AP satisfies_DES implies AP satisfies_TDES
  proof assume A1: AP satisfies_DES; thus AP satisfies_TDES
   proof let K,o,a,b,c,a',b',c';
    assume A2: K is_line & o in K & c in K & c' in K &
     not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' &
     a,b // a',b' & a,c // a',c' & a,b // K;

    A3: now assume o=b; then b in K & b,a // K by A2,AFF_1:48;
         hence contradiction by A2,AFF_1:37; end;
    set A=Line(o,a), P=Line(o,b);
    A4: A is_line & P is_line & o in A & a in A &
     o in P & b in P by A2,A3,AFF_1:38;
    then A5: a' in A & b' in P by A2,A3,AFF_1:39;
       A<>P proof assume A=P;
     then b in A & A // A by A4,AFF_1:55; then a,b // A by A4,AFF_1:54;
     then A // K by A2,AFF_1:67;
     hence contradiction by A2,A4,AFF_1:59; end;
    hence thesis by A1,A2,A3,A4,A5,Def4; end;
  end;

theorem
Th27: AP satisfies_TDES_1 implies AP satisfies_des_1
 proof assume A1: AP satisfies_TDES_1; thus AP satisfies_des_1 proof
  let A,P,C,a,b,c,a',b',c'; assume
  A2: A // P & a in A & a' in A & b in P & b' in P & c in C &
    c' in C & A is_line & P is_line & C is_line & A<>P & A<>C &
    a,b // a',b' & a,c // a',c' & b,c // b',c' &
    not LIN a,b,c & c <>c'; assume
  A3: not A // C; then consider o such that
  A4: o in A & o in C by A2,AFF_1:72; consider M such that
  A5: c in M & A // M by A2,AFF_1:63; consider N such that
  A6: c' in N & A // N by A2,AFF_1:63;
  A7: M is_line & N is_line & M // A & N // A
                            by A5,A6,AFF_1:50;
  A8: M // N & N // M & M // P & N // P by A2,A5,A6,AFF_1:58;
 A9: a<>b & b<>c & a<>c by A2,AFF_1:16;
  A10: a<>b' & a'<>b & a'<>b' by A2,AFF_1:59;
  A11: a<>a' proof assume A12: a=a';
   then LIN a,b,b' by A2,AFF_1:def 1; then LIN
 b,b',a by AFF_1:15; then b=b' or a in P
   by A2,AFF_1:39; then LIN b,c,c' & LIN
 a,c,c' by A2,A12,AFF_1:59,def 1;
   then LIN c,c',a & LIN c,c',b & LIN c,c',c by AFF_1:15,16;
   hence contradiction by A2,AFF_1:17; end;
  A13: b<>b' proof assume b=b';
   then b,a // b,a' by A2,AFF_1:13; then LIN b,a,a' by AFF_1:def 1;
   then LIN a,a',b by AFF_1:15; then b in A by A2,A11,AFF_1:39;
   hence contradiction by A2,AFF_1:59; end;
  A14: a'<>c' proof assume a'=c'; then b,c // a',b' by A2,AFF_1:13;
   then a,b // b,c by A2,A10,AFF_1:14; then b,a // b,c by AFF_1:13;
   then LIN b,a,c by AFF_1:def 1; hence contradiction by A2,AFF_1:15; end;
  set P'=Line(a,b), C'=Line(a',b');
  A15: P' is_line & C' is_line & b in P' & a in P' &
   b' in C' & a' in C' by A9,A10,AFF_1:38;
  A16: P' // C' by A2,A9,A10,AFF_1:51;
    not M // P' proof assume M // P'; then A // P' by A5,AFF_1:58;
   then b in A by A2,A15,AFF_1:59;
   hence contradiction by A2,AFF_1:59; end;
  then consider p such that A17: p in M & p in P' by A7,A15,AFF_1:72;
    not N // C' proof assume N // C'; then A // C' by A6,AFF_1:58;
   then b' in A by A2,A15,AFF_1:59;
   hence contradiction by A2,AFF_1:59; end;
  then consider q such that A18: q in N & q in C' by A7,A15,AFF_1:72;
    not P // C by A2,A3,AFF_1:58; then consider s such that
  A19: s in P & s in C by A2,AFF_1:72;
  A20: LIN s,c,c' by A2,A19,AFF_1:33;
  A21: c <>p by A2,A15,A17,AFF_1:33;
  A22: c,p // P by A5,A8,A17,AFF_1:54;
  A23: p,b // q,b' by A15,A16,A17,A18,AFF_1:53;
  A24: not c in P proof assume c in P; then c in P &
   c' in P by A2,A9,AFF_1:62;
  hence contradiction by A2,A3,AFF_1:30; end;
  A25: s<>b proof assume s=b; then b in C &
   b,c // c',b' by A2,A19,AFF_1:13; then b in C &
   b' in C by A2,A9,AFF_1:62;
   hence contradiction by A2,A3,A13,AFF_1:30; end;
  A26: c,p // c',q by A5,A6,A8,A17,A18,AFF_1:53;
    c,b // c',b' by A2,AFF_1:13;
  then A27: LIN s,p,q by A1,A2,A19,A20,A21,A22,A23,A24,A25,A26,Def8;
  A28: LIN o,c',c by A2,A4,AFF_1:33;
  A29: not c' in A proof assume c' in A; then c' in A &
   a',c' // a,c by A2,AFF_1:13; then c in A & c' in A by A2,A14,AFF_1:62;
hence contradiction by A2,AFF_1:30; end;
  A30: c',q // c,p by A5,A6,A8,A17,A18,AFF_1:53;
  A31: c',a' // c,a by A2,AFF_1:13; C' // P' by A16;
  then A32: q,a' // p,a by A15,A17,A18,AFF_1:53;
  A33: c',q // A by A6,A7,A18,AFF_1:54;
  A34: c'<>q proof assume c'=q;
   then LIN a',b',c' by A15,A18,AFF_1:33; then a',b' // a',c' by AFF_1:def 1;
   then a',b' // a,c by A2,A14,AFF_1:14; then a,b // a,c by A2,A10,AFF_1:14;
   hence contradiction by A2,AFF_1:def 1; end;
     o<>a' proof assume o=a'; then a' in C & a',c' // c,a
   by A2,A4,AFF_1:13; then a in C & a' in C by A2,A14,AFF_1:62;
   hence contradiction by A2,A11,AFF_1:30; end;
  then LIN o,q,p by A1,A2,A4,A28,A29,A30,A31,A32,A33,A34,Def8;
  then LIN p,q,o & LIN p,q,s & LIN p,q,p by A27,AFF_1:15,16;
  then A35: p=q or LIN o,s,p by AFF_1:17;
    now assume p=q; then M=N by A8,A17,A18,AFF_1:59;
   hence contradiction by A2,A3,A5,A6,A7,AFF_1:30; end;
  then o=s or p in C by A2,A4,A19,A35,AFF_1:39;
  then c in P' by A2,A3,A4,A5,A7,A17,A19,AFF_1:30,59
; hence contradiction by A2,A15,AFF_1:33; end;
 end;

theorem
   AP satisfies_TDES implies AP satisfies_des
 proof assume AP satisfies_TDES; then AP satisfies_TDES_1 by Th17;
  then AP satisfies_des_1 by Th27;
   hence thesis by Th21;
  end;

theorem
   AP satisfies_des implies AP satisfies_pap
 proof assume A1: AP satisfies_des; thus AP satisfies_pap
 proof let M,N,a,b,c,a',b',c';
  assume A2: M is_line & N is_line & a in M & b in M & c in M &
     M // N & M<>N & a' in N & b' in N & c' in N &
      a,b' // b,a' & b,c' // c,b';
  assume A3: not thesis;
  A4: b<>c' & c <>b' & a<>b' & b<>a' by A2,AFF_1:59;
  A5: a<>b & a<>c & b<>c proof
   A6: now assume A7: a=b;
    then LIN a,b',a' by A2,AFF_1:def 1; then LIN a',b',a by AFF_1:15;
    then a'=b' or a in N by A2,AFF_1:39;
    hence contradiction by A2,A3,A7,AFF_1:59; end;
   A8: now assume A9: a=c;
    then b,c' // b,a' by A2,A4,AFF_1:14; then LIN b,c',a' by AFF_1:def 1;
    then LIN a',c',b by AFF_1:15; then a'=c' or b in N by A2,AFF_1:39;hence
      contradiction by A2,A3,A9,AFF_1:11,59; end;
     now assume A10: b=c;
    then LIN b,c',b' by A2,AFF_1:def 1; then LIN b',c',b by AFF_1:15;
    then b'=c' or b in N by A2,AFF_1:39;
    hence contradiction by A2,A3,A10,AFF_1:59; end;
   hence thesis by A6,A8; end;
  A11: a'<>b' & a'<>c' & b'<>c' proof
   A12: now assume a'=b';
    then a',a // a',b by A2,AFF_1:13; then LIN a',a,b by AFF_1:def 1;
    then LIN a,b,a' by AFF_1:15; then a' in M by A2,A5,AFF_1:39;
    hence contradiction by A2,AFF_1:59; end;
   A13: now assume a'=c';
    then a,b' // c,b' by A2,A4,AFF_1:14; then b',a // b',c by AFF_1:13;
    then LIN b',a,c by AFF_1:def 1; then LIN a,c,b' by AFF_1:15;
    then b' in M by A2,A5,AFF_1:39;
    hence contradiction by A2,AFF_1:59; end;
      now assume b'=c';
     then b',b // b',c by A2,AFF_1:13; then LIN b',b,c by AFF_1:def 1;
     then LIN b,c,b' by AFF_1:15; then b' in M by A2,A5,AFF_1:39;
     hence contradiction by A2,AFF_1:59; end;
    hence thesis by A12,A13; end;
  set A=Line(a,b'), A'=Line(b,a'), P=Line(b,c'), P'=Line(c,b');
  A14: A is_line & A' is_line & P is_line & P' is_line &
   a in A & b' in A & b in A' & a' in A' & b in P & c' in P &
   c in P' & b' in P' by A4,AFF_1:38;
  then consider C such that A15: c in C & A // C by AFF_1:63;
  A16: C is_line & C // A by A15,AFF_1:50;
  consider C' such that A17: a in C' & P' // C' by A14,AFF_1:63;
  A18: C' is_line & C' // P' by A17,AFF_1:50;
    not C // C' proof assume C // C';
   then A // C' by A15,AFF_1:58; then A // P' by A17,AFF_1:58;
then b',a // b',c by A14,AFF_1:53;
   then LIN b',a,c by AFF_1:def 1; then LIN a,c,b' by AFF_1:15;
   then b' in M by A2,A5,AFF_1:39;
   hence contradiction by A2,AFF_1:59; end;
  then consider s such that
  A19: s in C & s in C' by A16,A18,AFF_1:72;
  A20: b',a // c,s by A14,A15,A19,AFF_1:53; N // M by A2;
  then A21: b',c' // c,b by A2,AFF_1:53;
  A22: P'<>P proof assume P'=P;
   then LIN b,c,b' by A14,AFF_1:33; then b' in M by A2,A5,AFF_1:39;
   hence contradiction by A2,AFF_1:59; end;
  A23: P'<>C' proof assume P'=C';
   then LIN a,c,b' by A14,A17,AFF_1:33; then b' in M by A2,A5,AFF_1:39;
   hence contradiction by A2,AFF_1:59; end;
    c,b' // b,c' by A2,AFF_1:13;
   then P' // P by A4,A14,AFF_1:52;
  then A24: c',a // b,s by A1,A14,A17,A18,A19,A20,A21,A22,A23,Def11;
  A25: a,b // b',a' by A2,AFF_1:53;
  A26: A<>A' proof assume A=A';
   then LIN a',b',a by A14,AFF_1:33; then a in N by A2,A11,AFF_1:39;
   hence contradiction by A2,AFF_1:59; end;
  A27: A<>C proof assume A=C;
   then LIN a,c,b' by A14,A15,AFF_1:33; then b' in M by A2,A5,AFF_1:39;
   hence contradiction by A2,AFF_1:59; end;
  A28: A // A' by A2,A4,AFF_1:51;
     a,s // b',c by A14,A17,A18,A19,AFF_1:53;
  then A29: b,s // a',c by A1,A14,A15,A16,A19,A25,A26,A27,A28,Def11;
    b<>s proof assume b=s; then a,b' // b,c by A14,A15,A19,AFF_1:53;
   then b,a' // b,c by A2,A4,AFF_1:14; then LIN b,a',c by AFF_1:def 1;
   then LIN b,c,a' by AFF_1:15; then a' in M by A2,A5,AFF_1:39;
   hence contradiction by A2,AFF_1:59; end;
  then c',a // a',c by A24,A29,AFF_1:14;
 hence contradiction by A3,AFF_1:13; end;
end;

Back to top