The Mizar article:

Affine Localizations of Desargues Axiom

by
Eugeniusz Kusak,
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

Received April 26, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: AFF_3
[ MML identifier index ]


environ

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

begin

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


definition let AP;
 attr AP is satisfying_DES1 means
    :Def1: for A,P,C,o,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & o in P & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & a<>a' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' holds a,c // p,q;
  synonym AP satisfies_DES1;
end;

definition let AP;
 attr AP is satisfying_DES1_1 means
    :Def2: for A,P,C,o,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & o in P & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        c <>q & not LIN b,a,c & not LIN b',a',c' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // p,q holds a,c // a',c';
  synonym AP satisfies_DES1_1;
end;

definition let AP;
 attr AP is satisfying_DES1_2 means
    :Def3: for A,P,C,o,a,a',b,b',c,c',p,q st
       A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & o in P & b in P & b' in P &
        c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & c <>c' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds o in C;
  synonym AP satisfies_DES1_2;
end;

definition let AP;
 attr AP is satisfying_DES1_3 means
    :Def4: for A,P,C,o,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & b<>b' & a<>a' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds o in P;
  synonym AP satisfies_DES1_3;
end;

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

definition let AP;
 attr AP is satisfying_DES2_1 means
    :Def6: for A,P,C,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
        a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p<>q &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // p,q holds a,c // a',c';
  synonym AP satisfies_DES2_1;
end;

definition let AP;
 attr AP is satisfying_DES2_2 means
    :Def7: for A,P,C,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
        a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // C & not LIN b,a,c & not LIN b',a',c' & p<>q & a<>a' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds A // P;
  synonym AP satisfies_DES2_2;
end;

definition let AP;
 attr AP is satisfying_DES2_3 means
    :Def8: for A,P,C,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
        a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // P & not LIN b,a,c & not LIN b',a',c' & p<>q & c <>c' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds A // C;
  synonym AP satisfies_DES2_3;
end;

canceled 8;

theorem
   AP satisfies_DES1 implies AP satisfies_DES1_1
 proof assume A1: AP satisfies_DES1;
 let A,P,C,o,a,a',b,b',c,c',p,q;
 assume that A2: A is_line & P is_line & C is_line and
     A3: P<>A & P<>C & A<>C and
     A4: o in A & a in A & a' in A & o in P & b in P &
      b' in P & o in C & c in C & c' in C & o<>a & o<>b & o<>c
      & p<>q & c <>q & not LIN b,a,c & not LIN b',a',c' and
     A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q;
 set K=Line(b,a); set M=Line(b,c);
    b<>a & b<>c & a<>c by A4,AFF_1:16;
 then A6: K is_line & M is_line & b in K & a in K & b in M & c in M &
     p in K & q in M by A5,AFF_1:26,def 2,def 3;
 A7: a'<>b' & b'<>c' & a'<>c' by A4,AFF_1:16;
 A8: M<>P & K<>P by A2,A3,A4,A6,AFF_1:30;
 A9: b<>o & b<>a & b<>c by A4,AFF_1:16;
 A10: K<>M by A4,A6,AFF_1:33;
 A11: not LIN o,a,c proof assume LIN o,a,c; then c in A
   by A2,A4,AFF_1:39;
   hence contradiction by A2,A3,A4,AFF_1:30; end;
     p<>b by A4,A5,AFF_1:69;
  then A12: p<>b' by A2,A4,A6,A8,AFF_1:30;
     q<>b proof assume A13: q=b;
     not LIN b,c,a & c,a // q,p & LIN b,c,q & LIN b,a,p by A4,A5,AFF_1:13,15;
   hence contradiction by A4,A13,AFF_1:69; end;
  then A14: q<>b' by A2,A4,A6,A8,AFF_1:30;
  A15: not LIN b',p,q proof assume LIN b',p,q; then A16: LIN p,q,b'
    by AFF_1:15; set N=Line(p,q);
    A17: N is_line & p in N & q in N & b' in N
      by A4,A16,AFF_1:26,def 2,def 3;
      LIN p,b',a' & LIN q,b',c' by A5,AFF_1:15;
     then a' in N & c' in N by A12,A14,A17,AFF_1:39;hence contradiction by A4,
A17,AFF_1:33; end;
A18:    a <> p by A4,A5,AFF_1:23;
    LIN o,a,a' & LIN b',p,a' & LIN o,c,c' & LIN b',q,c'
    by A2,A4,A5,AFF_1:15,33;
  hence thesis by A1,A2,A4,A5,A6,A7,A8,A9,A10,A11,A15,A18,Def1;
end;

theorem
   AP satisfies_DES1_1 implies AP satisfies_DES1
 proof assume A1: AP satisfies_DES1_1;
 let A,P,C,o,a,a',b,b',c,c',p,q;
 assume that A2: A is_line & P is_line & C is_line and
     A3: P<>A & P<>C & A<>C and
     A4: o in A & a in A & a' in A & o in P & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & a<>a' and
     A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
         a,c // a',c'; set K=Line(b,a); set M=Line(b,c);
    b<>a & b<>c & a<>c by A4,AFF_1:16;
 then A6: K is_line & M is_line & b in K & a in K & b in M & c in M &
     p in K & q in M by A5,AFF_1:26,def 2,def 3;
 A7: a'<>b' & b'<>c' & a'<>c' by A4,AFF_1:16;
 A8: K<>P by A2,A3,A4,A6,AFF_1:30;
 A9: M<>P by A2,A3,A4,A6,AFF_1:30;
 A10: M<>P & K<>P by A2,A3,A4,A6,AFF_1:30;
 A11: b<>o & b<>a & b<>c by A4,AFF_1:16;
 A12: K<>M by A4,A6,AFF_1:33;
 A13: not LIN o,a,c proof assume LIN o,a,c; then c in A
   by A2,A4,AFF_1:39;
   hence contradiction by A2,A3,A4,AFF_1:30; end;
 A14: c <>c' proof assume c =c';
  then c,a // c,a' & LIN o,a,a' & not LIN o,c,a
   by A2,A4,A5,A13,AFF_1:13,15,33;
    hence contradiction by A4,AFF_1:23; end;
 A15: now assume A16: not LIN b',p,q;
     LIN o,a,a' & LIN b',p,a' & LIN o,c,c' & LIN b',q,c'
    by A2,A4,A5,AFF_1:15,33;
  hence thesis by A1,A2,A4,A5,A6,A7,A10,A11,A12,A13,A14,A16,Def2; end;
    now assume A17: LIN b',p,q; set A'=Line(b',a'); set C'=Line(b',c');
  A18: LIN b',q,p by A17,AFF_1:15;
  A19: A' is_line & C' is_line & b' in A' & a' in A' & p in A' &
   b' in C' & c' in C' & q in C' by A5,A7,AFF_1:26,def 2,def 3;
  then A20: A'<>C' by A4,AFF_1:33;

  A21: now assume b'<>p; then A22: q in A' by A17,A19,AFF_1:39;
      then A23: q=b' by A19,A20,AFF_1:30; LIN
 b,c,b' by A5,A19,A20,A22,AFF_1:30;
then b' in M
      by AFF_1:def 2; then A24: b=b' by A2,A4,A6,A9,AFF_1:30;
      A'<>K proof assume A'=K; then LIN a,a',b by A6,A19,AFF_1:33;
      then b in A by A2,A4,AFF_1:39;
     hence contradiction by A2,A3,A4,AFF_1:30; end;
     then p=q by A6,A19,A23,A24,AFF_1:30;
    hence thesis by AFF_1:12; end;

     now assume b'<>q; then A25: p in C' by A18,A19,AFF_1:39;
     then A26: p=b' by A19,A20,AFF_1:30; LIN b,a,b' by A5,A19,A20,A25,AFF_1:30
;
then b' in K
     by AFF_1:def 2; then A27: b=b' by A2,A4,A6,A8,AFF_1:30;
      C'<>M proof assume C'=M; then LIN c,c',b by A6,A19,AFF_1:33;
      then b in C by A2,A4,A14,AFF_1:39;
     hence contradiction by A2,A3,A4,AFF_1:30; end;
     then p=q by A6,A19,A26,A27,AFF_1:30;
    hence thesis by AFF_1:12; end;

  hence thesis by A4,A21; end;

 hence thesis by A15;
end;

theorem
   AP satisfies_DES implies AP satisfies_DES1
 proof assume A1: AP satisfies_DES;
 let A,P,C,o,a,a',b,b',c,c',p,q;
 assume that A2: A is_line & P is_line & C is_line and
     A3: P<>A & P<>C & A<>C and
     A4: o in A & a in A & a' in A & o in P & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & a<>a' and
     A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c';
 set K=Line(b',a'); set M=Line(b',c');
 A6: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A4,AFF_1:16;
 then A7: K is_line & M is_line & b' in K & a' in K & p in K &
     b' in M & c' in M & q in M by A5,AFF_1:26,def 2,def 3;
 A8: not LIN o,a,c proof assume LIN o,a,c; then c in A
      by A2,A4,AFF_1:39; hence
        contradiction by A2,A3,A4,AFF_1:30; end;
 A9: o<>a' proof assume A10: o=a';
        LIN o,a,a' & LIN o,c,c' by A2,A4,AFF_1:33;
      hence
        contradiction by A5,A6,A8,A10,AFF_1:69; end;
 A11: o<>c' proof assume A12: o=c';
        LIN o,a,a' & LIN o,c,c' & c,a // c',a' & not LIN o,c,a
      by A2,A4,A5,A8,AFF_1:13,15,33;
      hence contradiction by A9,A12,AFF_1:69; end;
 A13: c <>c' proof assume c =c';
      then LIN o,a,a' & c,a // c,a' & not LIN o,c,a
      by A2,A4,A5,A8,AFF_1:13,15,33;
      hence contradiction by A4,AFF_1:23; end;
 A14: K<>P & M<>P & K<>M by A2,A3,A4,A7,A9,A11,AFF_1:30,33;
set D=Line(b,c); A15: D is_line & b in D & c in D & q in D
                                   by A5,A6,AFF_1:26,def 2,def 3;
then consider D' such that A16: c' in D' & D // D' by AFF_1:63;
   A17: D' is_line & D' // D by A16,AFF_1:50;
    not D' // P proof assume D' // P; then D // P
       by A16,AFF_1:58; then c in P
       by A4,A15,AFF_1:59; hence
         contradiction by A2,A3,A4,AFF_1:30; end; then consider d such that
  A18: d in D' & d in P by A2,A17,AFF_1:72;
  A19: d<>b' proof assume d=b'; then M=D'
       by A6,A7,A16,A17,A18,AFF_1:30; then D=M
       by A7,A15,A16,AFF_1:59; then LIN c,c',b by A7,A15,AFF_1:33;
       then b in C by A2,A4,A13,AFF_1:39;
       hence contradiction by A2,A3,A4,AFF_1:30; end;

   c,b // c',d & c,a // c',a' by A5,A15,A16,A18,AFF_1:13,53;

 then A20: b,a // d,a' by A1,A2,A3,A4,A18,AFF_2:def 4;
   b,a // b,p by A5,AFF_1:def 1;
 then d,a' // b,p & b,q // d,c' by A6,A15,A16,A18,A20,AFF_1:14,53;
then d,a' // b,p & d,c' // b,q by AFF_1:13;
 then a',c' // p,q by A1,A2,A4,A6,A7,A14,A18,A19,AFF_2:def 4;
 hence thesis by A5,A6,AFF_1:14;
end;

theorem
   AP satisfies_DES implies AP satisfies_DES1_2
proof assume A1: AP satisfies_DES;
 then A2: AP satisfies_DES_1 by AFF_2:16;
 let A,P,C,o,a,a',b,b',c,c',p,q;
 assume that A3: A is_line & P is_line & C is_line and
     A4: P<>A & P<>C & A<>C and
     A5: o in A & a in A & a' in A & o in P & b in P &
       b' in P & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
       not LIN b,a,c & not LIN b',a',c' & c <>c' and
     A6: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
       a,c // a',c' & a,c // p,q;
  A7: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A5,AFF_1:16;
  A8: b'<>a' & b'<>c' by A5,AFF_1:16;
set K=Line(b',a'); set M=Line(b',c');
  A9: K is_line & M is_line & b' in K & a' in K & p in K &
      b' in M & c' in M & q in M by A6,A7,AFF_1:26,def 2,def 3;
  then A10: K<>M by A5,AFF_1:33;
  A11:  b<>q proof assume A12: b=q; not LIN b,c,a & c,a // q,p
      by A5,A6,AFF_1:13,15;
      hence contradiction by A5,A6,A12,AFF_1:69; end;
  A13: b'<>q proof assume A14: b'=q; a',c' // p,q by A6,A7,AFF_1:14;
      then c',a' // q,p & not LIN b',c',a' by A5,AFF_1:13,15;hence
        contradiction by A5,A6,A14,AFF_1:69; end;
  A15: b'<>p proof assume A16: b'=p; a',c' // p,q by A6,A7,AFF_1:14;
      hence
        contradiction by A5,A6,A16,AFF_1:69; end;
  A17: b<>p by A5,A6,AFF_1:69;
  now
  A18: now assume A19: M=P;
        LIN b,q,c by A6,AFF_1:15; then c in P by A5,A9,A11,A19,AFF_1:39;
      then P=Line(c,c') by A5,A9,A19,AFF_1:71;
      hence thesis by A3,A5,AFF_1:71; end;

     now assume A20: M<>P; set D=Line(b,c);

    A21: D is_line & b in D & c in D & q in D
      by A6,A7,AFF_1:26,def 2,def 3; then consider D' such that
    A22: c' in D' & D // D' by AFF_1:63;
    A23: D' is_line by A22,AFF_1:50;
      not D' // P proof assume D' // P; then D // P
      by A22,AFF_1:58; then q in P
      by A5,A21,AFF_1:59; hence
        contradiction by A3,A5,A9,A13,A20,AFF_1:30
; end; then consider d such that
    A24: d in D' & d in P by A3,A23,AFF_1:72;
    A25: q,b // c',d & b,c // d,c' by A21,A22,A24,AFF_1:53;
    then A26: c',d // q,b & b,c // d,c' by AFF_1:13;
    A27: d<>b' proof assume d=b';
      then M=D' by A7,A9,A22,A23,A24,AFF_1:30;
      then D=M by A9,A21,A22,AFF_1:59;
      then LIN c,c',b & LIN c,c',b' by A9,A21,AFF_1:33; then A28: b in C &
      b' in C by A3,A5,AFF_1:39;
     set T=Line(b,a); set N=Line(a,c);
      A29: T is_line & b in T & a in T & p in T
                                    by A6,A7,AFF_1:26,def 2,def 3;
      A30: N is_line & a in N & c in N by A7,AFF_1:26,def 3;
       A31: a<>a' proof assume a=a'; then LIN a,c,c'
        by A6,AFF_1:def 1;
 then c' in N
        by AFF_1:def 2; then N=C by A3,A5,A30,AFF_1:30;
hence contradiction by A5,A28,A30,AFF_1:33; end;
          b<>b' proof assume A32: b=b';
           K<>T proof assume K=T; then T=A by A3,A5,A9,A29,A31,AFF_1:30;
hence
           contradiction by A3,A4,A5,A29,AFF_1:30; end;
        hence contradiction by A9,A15,A29,A32,AFF_1:30; end;
      hence contradiction by A3,A4,A5,A28,AFF_1:30; end;

   p,q // a',c' by A6,A7,AFF_1:14; then c',a' // q,p by AFF_1:13;
then A33: d,a' // b,p by A1,A3,A5,A8,A9,A10,A20,A24,A26,A27,AFF_2:def 4;

   b,a // b,p by A6,AFF_1:def 1;
 then b,a // d,a' by A17,A33,AFF_1:14;
  hence thesis by A2,A3,A4,A5,A6,A24,A25,AFF_2:def 5; end;
 hence thesis by A18; end;
hence thesis;
end;

theorem
   AP satisfies_DES1_2 implies AP satisfies_DES1_3
proof assume A1: AP satisfies_DES1_2;
 let A,P,C,o,a,a',b,b',c,c',p,q;
assume that A2:A is_line & P is_line & C is_line and
   A3: P<>A & P<>C & A<>C and
   A4: o in A & a in A & a' in A & b in P & b' in P &
       o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
       not LIN b,a,c & not LIN b',a',c' & b<>b' & a<>a' and
   A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
       a,c // a',c' & a,c // p,q;
assume A6: not thesis;
 A7: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A4,AFF_1:16;
 A8: not LIN o,c,a proof assume LIN o,c,a; then a in C
      by A2,A4,AFF_1:39;
                 hence contradiction by A2,A3,A4,AFF_1:30; end;
 A9: c <>c' proof assume c =c';
      then LIN o,a,a' & c,a // c,a' by A2,A4,A5,AFF_1:13,33;
hence contradiction by A4,A8,AFF_1:23; end;
 A10: a',c' // p,q by A5,A7,AFF_1:14;
 A11: p<>b & p<>b' & q<>b & q<>b' proof assume A12: not thesis;
    A13: now assume A14: b=q; not LIN b,c,a & c,a // q,p
        by A4,A5,AFF_1:13,15; hence
          contradiction by A4,A5,A14,AFF_1:69; end;
       now assume A15: b'=q; not LIN b',c',a' & c',a' // q,p
        by A4,A10,AFF_1:13,15; hence
          contradiction by A4,A5,A15,AFF_1:69; end;
    hence contradiction by A4,A5,A10,A12,A13,AFF_1:69; end;

 A16: not P // A or not C // P proof assume not thesis;
    then C // A by AFF_1:58; hence
      contradiction by A3,A4,AFF_1:59; end;
set D=Line(b,c), T=Line(b,a), N=Line(p,q), M=Line(a',c'), K=Line(b',a');
 A17: D is_line & T is_line & N is_line & M is_line &
  K is_line & p in N & q in N & b in D & c in D &
  b in T & a in T & a' in M & c' in M & b' in K &
  a' in K by A4,A7,AFF_1:38;
 then A18: q in D & p in T & p in K by A5,A7,AFF_1:39;

 A19: now assume not P // A; then consider x such that
    A20: x in P & x in A by A2,AFF_1:72;
    A21: x<>a proof assume A22: x=a;
     then A23: p in P & a in P by A2,A4,A5,A7,A20,AFF_1:39;
         K<>P by A2,A3,A4,A17,A20,A22,AFF_1:30;
       hence contradiction by A2,A4,A11,A17,A18,A23,AFF_1:30; end;
       x<>b proof assume A24: x=b;
     then LIN b,a,a' & LIN b,a,a by A2,A4,A20,AFF_1:33; then LIN a,a',p
     by A5,A7,AFF_1:17; then p in A by A2,A4,AFF_1:39;
then a',c' // a',q or b' in A by A2,A4,A10,A17,A18,AFF_1:30
; then LIN a',c',q by A2,A3,A4,A20,A24,AFF_1:30,def 1;
     then LIN q,c',a' & LIN q,c',b' & LIN q,c',c' by A5,AFF_1:15,16;
     then q=c' by A4,AFF_1:17; then LIN c,c',b by A5,AFF_1:15; then b in C
by A2,A4,A9,AFF_1:39;
     hence contradiction by A2,A3,A4,A20,A24,AFF_1:30; end;
 then x in C by A1,A2,A3,A4,A5,A9,A20,A21,Def3;
  hence contradiction by A2,A3,A4,A6,A20,AFF_1:30; end;

    now assume not C // P; then consider x such that
    A25: x in C & x in P by A2,AFF_1:72;
    A26: x<>c proof assume A27: x=c;
     then LIN b,c,b' & LIN b,c,c by A2,A4,A25,AFF_1:33; then LIN q,b',c &
     LIN q,b',c' & LIN q,b',b' by A5,A7,AFF_1:15,17; then LIN c,c',b'
     by A11,AFF_1:17; then A28: b' in C by A2,A4,A9,AFF_1:39;
     then A29: c =b' by A2,A3,A4,A25,A27,AFF_1:30; LIN c,c',q by A2,A3,A4,A5,
A25,A27,A28,AFF_1:30;
     then q in C by A2,A4,A9,AFF_1:39; then C=D by A2,A4,A11,A17,A18,A29,AFF_1:
30;
     hence contradiction by A2,A3,A4,A17,A28,AFF_1:30; end;
    A30: x<>b proof assume A31: x=b;
     then LIN b,c,c' & LIN b,c,c by A2,A4,A25,AFF_1:33;
     then LIN c,c',q by A5,A7,AFF_1:17;
     then q in C & LIN q,c',b' by A2,A4,A5,A9,AFF_1:15,39;
     then q=c' or b' in C by A2,A4,AFF_1:39; then c',a' // c',p
     by A2,A3,A4,A10,A25,A31,AFF_1:13,30; then LIN c',a',p by AFF_1:def 1;
     then LIN p,a',c' & LIN p,a',b' & LIN p,a',a' by A5,AFF_1:15,16;
     then p=a' by A4,AFF_1:17; then LIN a,a',b by A5,AFF_1:15; then b in A
by A2,A4,AFF_1:39; hence contradiction by A2,A3,A4,A25,A31,AFF_1:30; end;
     A32: not LIN b,c,a & not LIN b',c',a' by A4,AFF_1:15;
  c,a // q,p & c,a // c',a' by A5,AFF_1:13;
 then x in A by A1,A2,A3,A4,A5,A25,A26,A30,A32,Def3;
  hence contradiction by A2,A3,A4,A6,A25,AFF_1:30; end;

 hence contradiction by A16,A19;
end;

theorem
   AP satisfies_DES1_2 implies AP satisfies_DES
proof assume A1: AP satisfies_DES1_2;
 let A,P,C,o,a,b,c,a',b',c';
assume that A2: 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 and
     A3: A is_line & P is_line & C is_line and
     A4: A<>P & A<>C and A5: a,b // a',b' & a,c // a',c';
  now assume A6: P<>C;
 then A7: a<>b & a<>c & b<>c by A2,A3,A4,AFF_1:30;
  A8: not LIN o,b,a & not LIN o,a,c proof assume A9: not thesis;
     A10: now assume LIN o,b,a; then a in P by A2,A3,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
        now assume LIN o,a,c; then c in A by A2,A3,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
    hence thesis by A9,A10; end;

 A11: a'=o implies thesis proof assume A12: a'=o;
       LIN o,a,a' & LIN o,c,c' & not LIN o,a,c by A2,A3,A8,AFF_1:33;
     then A13: o=c' by A5,A12,AFF_1:69;
       LIN o,a,a' & LIN o,b,b' & not LIN o,a,b by A2,A3,A8,AFF_1:15,33;
     then o=b' by A5,A12,AFF_1:69;
    hence thesis by A13,AFF_1:12; end;

 A14: b'=o implies thesis proof assume A15: b'=o;
       LIN o,b,b' & LIN o,a,a' & not LIN o,b,a & b,a // b',a'
     by A2,A3,A5,A8,AFF_1:13,33;
    hence thesis by A11,A15,AFF_1:69; end;

 A16: c'=o implies thesis proof assume A17: c'=o;
       LIN o,c,c' & LIN o,a,a' & not LIN o,c,a & c,a // c',a'
     by A2,A3,A5,A8,AFF_1:13,15,33;
    hence thesis by A11,A17,AFF_1:69; end;
set K=Line(a,c);
   A18: K is_line & a in K & c in K by A7,AFF_1:26,def 3;

 A19: LIN a,b,c implies thesis proof assume LIN a,b,c;
     then LIN a,c,b by AFF_1:15; then A20: b in K by AFF_1:def 2;
      then K=Line(a,b) & K=Line(b,c) by A7,A18,AFF_1:71;
     then a,c // K & a,b // K by A7,AFF_1:43;
     then A21: a',c' // K & a',b' // K by A5,A7,AFF_1:46;
    consider N such that A22: a' in N & K // N by A18,AFF_1:63;
     A23: N is_line by A22,AFF_1:50;
       a',c' // N & a',b' // N by A21,A22,AFF_1:57;
     then c' in N & b' in N by A22,A23,AFF_1:37;hence thesis by A18,A20,A22,
AFF_1:53; end;

 A24: b=b' implies thesis proof assume A25: b=b';
     then LIN o,a,a' & not LIN o,b,a & b,a // b,a'
     by A2,A3,A5,A8,AFF_1:13,33;
     then LIN o,c,c' & not LIN o,a,c & a,c // a,c'
     by A2,A3,A5,A8,AFF_1:23,33; then c =c' by AFF_1:23;
     hence thesis by A25,AFF_1:11; end;

    now assume
                A26: o<>a' & o<>b' & o<>c' & b<>b' & not LIN a,b,c;
  then A27: a'<>b' & a'<>c' & b'<>c' by A2,A3,A4,A6,AFF_1:30;
 assume not b,c // b',c'; then consider q such that
  A28: LIN b,c,q & LIN b',c',q by AFF_1:74; consider M such that
  A29: q in M & K // M by A18,AFF_1:63;
  A30: M is_line by A29,AFF_1:50;
    not a,b // M proof assume a,b // M;
    then a,b // K by A29,AFF_1:57;
    then b in K by A18,AFF_1:37;hence contradiction by A18,A26,AFF_1:33;
  end;
 then consider p such that
                           A31: p in M & LIN a,b,p by A30,AFF_1:73;
 set N=Line(a',c');
  A32: N is_line & a' in N & c' in N by A27,AFF_1:26,def 3;
  A33: K // N by A5,A7,A27,AFF_1:51;
  then A34: N // M by A29,AFF_1:58;
  A35: not LIN a',b',c' proof assume LIN a',b',c';
     then LIN a',c',b' by AFF_1:15; then b' in N by AFF_1:def 2; then a',b'
// N
     by A32,AFF_1:37; then A36: a',b' // K by A33,AFF_1:57;
       a',b' // a,b by A5,AFF_1:13; then a,b // K by A27,A36,AFF_1:46;
     then b in K by A18,AFF_1:37;
     hence contradiction by A18,A26,AFF_1:33; end;
  A37: a<>a' proof assume a=a';
   then not LIN o,a,b & LIN o,b,b' & a,b // a,b' by A2,A3,A5,A8,AFF_1:15,33;
     hence contradiction by A26,AFF_1:23; end;
  A38: c <>c' proof assume c =c'; then not LIN o,c,a & LIN o,a,a' &
     c,a // c,a' by A2,A3,A5,A8,AFF_1:13,15,33;
     hence contradiction by A37,AFF_1:23; end;
  A39: A<>K by A2,A3,A4,A18,AFF_1:30;
    not b',p // N proof assume b',p // N; then b',p // M
     by A34,AFF_1:57; then p,b' // M by AFF_1:48;
     then A40: b' in M by A30,A31,AFF_1:37;
    A41: now assume b'=q; then LIN b,b',c
      by A28,AFF_1:15; then c in
 P by A2,A3,A26,AFF_1:39;hence contradiction by A2,A3,A6,AFF_1:30; end;
       now assume A42: b'<>q; LIN b',q,c' by A28,AFF_1:15; then c' in M
      by A29,A30,A40,A42,AFF_1:39;
      then a' in N & b' in N & c' in
 N by A32,A34,A40,AFF_1:59;hence contradiction by A32,A35,AFF_1:33; end;
    hence thesis by A41; end; then consider x such that
   A43: x in N & LIN b',p,x by A32,AFF_1:73;
   A44: LIN b',x,p by A43,AFF_1:15;
   A45: x<>a proof assume x=a;
     then a in K & a' in K by A18,A32,A33,A43,AFF_1:59;
     then A=K by A2,A3,A18,A37,AFF_1:30;
     hence contradiction by A2,A3,A4,A18,AFF_1:30; end;
 set A'=Line(x,a);
    A46: A' is_line & x in A' & a in A' by A45,AFF_1:26,def 3;
    A47: p<>q proof assume A48: p=q; then LIN p,b,c & LIN p,b,a &
     LIN p,b,b by A28,A31,AFF_1:15,16; then p=b by A26,AFF_1:17;
     then LIN b,b',c' by A28,A48,AFF_1:15; then c' in P by A2,A3,A26,AFF_1:39
;
     hence contradiction by A2,A3,A6,A26,AFF_1:30; end;
    A49: not LIN b',c',x proof assume LIN b',c',x;
then A50:     LIN c',x,b' & LIN c',x,a' & LIN c',x,c'
                            by A32,A43,AFF_1:15,33;
     then A51: c'=x or LIN b',c',a' by AFF_1:17;
A52:     now assume c'=x; then LIN b',c',p & LIN b',c',c'
                                     by A43,AFF_1:15,16;
      then LIN p,q,c' by A27,A28,AFF_1:17; then c' in M by A29,A30,A31,A47,
AFF_1:39;
      then q in N & LIN q,c',b' by A28,A29,A32,A34,AFF_1:15,59
; then A53: q=c' or b' in N
      by A32,AFF_1:39;
        now assume q=c'; then LIN c,c',b by A28,AFF_1:15; then b in C by A2,A3,
A38,AFF_1:39; hence contradiction by A2,A3,A6,AFF_1:30; end;
      hence LIN b',c',a' by A32,A53,AFF_1:33; end;
      then b',c' // b',a' by A51,AFF_1:def 1;
     then b',c' // a',b' by AFF_1:13; then A54: b',c' // a,b by A5,A27,AFF_1:14
; LIN c',a',b' by A50,A52,AFF_1:15,17;
     then c',a' // c',b' by AFF_1:def 1; then a',c' // b',c' by AFF_1:13;
     then a,c // b',c' by A5,A27,AFF_1:14;
     then a,c // a,b by A27,A54,AFF_1:14; then LIN a,c,b by AFF_1:def 1;
     hence contradiction by A26,AFF_1:15; end;
     A55: c,a // c',x by A18,A32,A33,A43,AFF_1:53;
     A56: c,a // q,p by A18,A29,A31,AFF_1:53;
   not LIN b,c,a & LIN b,a,p by A26,A31,AFF_1:15;
  then o in A' by A1,A2,A3,A6,A28,A44,A45,A46,A47,A49,A55,A56,Def3;
  then A57: x in A by A2,A3,A46,AFF_1:30;
      A <> N by A2,A18,A33,A39,AFF_1:59;
   then A58: x=a' by A2,A3,A32,A43,A57,AFF_1:30;
   set D=Line(b,a); set T=Line(b',a');
       A59: D is_line & T is_line & b in D & a in D & p in D &
           b' in T & a' in T & p in T
                by A7,A27,A31,A44,A58,AFF_1:26,def 2,def 3;
         D // T by A5,A7,A27,AFF_1:51;
then a in D & a' in D by A59,AFF_1:59; then b in A by A2,A3,A37,A59,AFF_1:30;
hence contradiction by A2,A3,A4,AFF_1:30;
  end;
hence thesis by A11,A14,A16,A19,A24; end;
hence thesis by A2,A3,AFF_1:65;
end;

theorem
   AP satisfies_DES2_1 implies AP satisfies_DES2
 proof assume A1: AP satisfies_DES2_1;
  let A,P,C,a,a',b,b',c,c',p,q;
 assume that A2: A is_line & P is_line & C is_line and
     A3: A<>P & A<>C & P<>C and
     A4: a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // P & A // C & not LIN b,a,c & not LIN b',a',c' &
        p<>q & a<>a'
 and A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c';
 A6: P // C by A4,AFF_1:58;
 A7: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A4,AFF_1:16;
set K=Line(a,c), N=Line(a',c'), D=Line(b,c), T=Line(b',c');
 A8: K is_line & N is_line & D is_line & T is_line &
      a in K & c in K & a' in N & c' in N & b in D &
     c in D & q in D & b' in T & c' in T & q in T
                                   by A5,A7,AFF_1:26,def 2,def 3;
 A9: K // N by A5,A7,AFF_1:51;
 A10: K<>A by A3,A4,A8,AFF_1:59;
 A11: c <>c' proof assume c =c';
  then K=N by A8,A9,AFF_1:59;hence contradiction by A2,A4,A8,A10,AFF_1:30
; end;
 A12: D<>T proof assume D=T; then D=C by A2,A4,A8,A11,AFF_1:30;hence
 contradiction by A3,A4,A6,A8,AFF_1:59; end;
  set A'=Line(b,a); set P'=Line(b',a'); A13: A' is_line & P' is_line &
     b in A' & a in A' & p in A' & b' in P' & a' in P' & p in P'
                                     by A5,A7,AFF_1:26,def 2,def 3;
 A14: b<>b' proof assume A15: b=b';
  then A16: b'=q by A8,A12,AFF_1:30;
        A'<>P' proof assume A'=P';
      then A'=A by A2,A4,A13,AFF_1:30;hence contradiction by A3,A4,A13,AFF_1:59
; end;
     hence contradiction by A4,A13,A15,A16,AFF_1:30; end;
consider M such that
 A17: p in M & N // M by A8,AFF_1:63; A18: M is_line by A17,AFF_1:50;
                                 A19: K // M by A9,A17,AFF_1:58;
 A20: not M // D or not T // M proof assume not thesis;
   then T // D by AFF_1:58; hence
     contradiction by A8,A12,AFF_1:59; end;

 A21: now assume not M // D; then consider x such that
    A22: x in M & x in D by A8,A18,AFF_1:72;
      not b',x // C proof assume A23: b',x // C;
    C // P by A4,AFF_1:58; then b',x // P by A23,AFF_1:57; then x in P by A2,A4
,AFF_1:37;
      then x=b or D=P by A2,A4,A8,A22,AFF_1:30;
     then A24: b=p or M=A'
     by A3,A4,A6,A8,A13,A17,A18,A22,AFF_1:30,59;
       now assume b=p; then LIN b,b',a' by A13,AFF_1:33; then a' in P
                                        by A2,A4,A14,AFF_1:39;
      hence contradiction by A3,A4,AFF_1:59; end;
     then b in K by A8,A13,A19,A24,AFF_1:59
; hence contradiction by A4,A8,AFF_1:33; end;
    then consider y such that
    A25: y in C & LIN b',x,y by A2,AFF_1:73;
   A26: LIN b',y,x & LIN b,c,x & a,c // p,x
                     by A8,A17,A19,A22,A25,AFF_1:15,33,53;
  A27: not LIN b',a',y proof assume LIN b',a',y;
   then LIN b',y,a' & LIN b',y,b' by AFF_1:15,16; then b'=y or
   LIN a',b',x by A26,AFF_1:17; then x in P' by A3,A4,A6,A25,AFF_1:59,def 2;
   then A28: x=p or P'=M by A13,A17,A18,A22,AFF_1:30;
     now assume x=p; then p=b or D=A'
    by A8,A13,A22,AFF_1:30; then LIN
 b,b',a' or c in A' by A13,AFF_1:26,33;
    then a' in P by A2,A4,A14,AFF_1:39,def 2;
    hence contradiction by A3,A4,AFF_1:59; end; then N=P' by A8,A13,A17,A28,
AFF_1:59
;hence contradiction by A4,A8,AFF_1:def 2; end;
    p<>x proof assume p=x; then p=b or D=A'
   by A8,A13,A22,AFF_1:30; then LIN b,b',a' or c in
 A' by A13,AFF_1:26,33;
   then a' in P by A2,A4,A14,AFF_1:39,def 2;
   hence contradiction by A3,A4,AFF_1:59; end;
   then a,c // a',y by A1,A2,A3,A4,A5,A25,A26,A27,Def6;
  then a',y // a',c' by A5,A7,AFF_1:14; then LIN a',y,c' by AFF_1:def 1;
  then LIN a',c',y by AFF_1:15; then y in N by AFF_1:def 2;
  then N=C or y=c' by A2,A4,A8,A25,AFF_1:30; then a' in C or
  LIN b',c',x by A25,AFF_1:15,26; then x in T by A3,A4,AFF_1:59,def 2;
  then q in M or
  c' in D by A8,A22,AFF_1:30; then a,c // p,q or LIN c,c',b
                                by A8,A17,A19,AFF_1:33,53;
  then a,c // p,q or b in C by A2,A4,A11,AFF_1:39;
 hence thesis by A3,A4,A6,AFF_1:59; end;

    now assume not T // M; then consider x such that
  A29: x in T & x in M by A8,A18,AFF_1:72;
    not b,x // C proof assume b,x // C; then b,x // C &
   C // P by A4,AFF_1:58; then b,x // P by AFF_1:57;
   then x in P by A2,A4,AFF_1:37; then b' in M or
   c' in P by A2,A4,A8,A29,AFF_1:30;
   then b'=p or M=P' by A3,A4,A6,A13,A17,A18,AFF_1:30,59;
   then LIN b,b',a or N // P' by A5,A17,AFF_1:15;
   then a in P or N=P' by A2,A4,A8,A13,A14,AFF_1:39,59;
   hence contradiction by A3,A4,A8,AFF_1:59,def 2; end;
  then consider y such that
  A30: y in C & LIN b,x,y by A2,AFF_1:73;
  A31: LIN b,y,x & LIN b',c',x & a',c' // p,x
                     by A8,A17,A29,A30,AFF_1:15,33,53;
  A32: not LIN b,a,y proof assume LIN b,a,y;
   then LIN b,y,a & LIN b,y,b by AFF_1:15,16; then b=y or
   LIN a,b,x by A31,AFF_1:17; then x in A' by A3,A4,A6,A30,AFF_1:59,def 2;
   then A33: x=p or A'=M by A13,A17,A18,A29,AFF_1:30;
     now assume x=p; then p=b' or T=P'
    by A8,A13,A29,AFF_1:30; then LIN
 b,b',a or c' in P' by A13,AFF_1:26,33;
    then a in P by A2,A4,A14,AFF_1:39,def 2;
    hence contradiction by A3,A4,AFF_1:59; end; then K=A' by A8,A13,A19,A33,
AFF_1:59;hence contradiction by A4,A8,AFF_1:def 2; end;
   p<>x proof assume p=x; then p=b' or T=P'
    by A8,A13,A29,AFF_1:30; then LIN
 b,b',a or c' in P' by A13,AFF_1:26,33;
    then a in P by A2,A4,A14,AFF_1:39,def 2;
    hence contradiction by A3,A4,AFF_1:59; end;
   then a',c' // a,y by A1,A2,A3,A4,A5,A30,A31,A32,Def6;
  then a,c // a,y by A5,A7,AFF_1:14; then LIN a,c,y by AFF_1:def 1;
  then y in K by AFF_1:def 2; then K=C or y=c by A2,A4,A8,A30,AFF_1:30;
then a in C or LIN b,c,x by A30,AFF_1:15,26;
  then x in D by A3,A4,AFF_1:59,def 2; then q in M or c' in D by A8,A29,AFF_1:
30;
  then a,c // p,q or LIN c,c',b by A8,A17,A19,AFF_1:33,53;
  then a,c // p,q or b in C by A2,A4,A11,AFF_1:39;
 hence thesis by A3,A4,A6,AFF_1:59; end;
 hence thesis by A20,A21;
end;

theorem
   AP satisfies_DES2_1 iff AP satisfies_DES2_3 proof
 A1: AP satisfies_DES2_1 implies AP satisfies_DES2_3
  proof assume A2: AP satisfies_DES2_1;
     thus AP satisfies_DES2_3 proof let A,P,C,a,a',b,b',c,c',p,q;
      assume A3: A is_line & P is_line & C is_line &
     A<>P & A<>C & P<>C & a in A & a' in A & b in P &
     b' in P & c in C & c' in C & A // P & not LIN b,a,c &
     not LIN b',a',c' & p<>q & c <>c' & LIN b,a,p & LIN b',a',p &
     LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q;

      now A4: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A3,AFF_1:16;
    set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
    A5: A' is_line & P' is_line & C' is_line & a in A' & c in A'
     & p in P' & q in P' & a' in C' & c' in C' by A3,A4,AFF_1:38;
    A6: q<>c proof assume A7: q=c; then c,p // c,a by A3,AFF_1:13;
     then LIN c,p,a by AFF_1:def 1; then LIN p,a,c & LIN p,a,b & LIN p,a,a
by A3,AFF_1:15,16; then a=p by A3,AFF_1:17;
     then LIN a,a',b' by A3,AFF_1:15; then b' in A or a=a' by A3,AFF_1:39;
     then a',c' // a',c by A3,AFF_1:13,59;
     then LIN a',c',c by AFF_1:def 1; then LIN c,c',a' by AFF_1:15;
     then A8: a' in C by A3,AFF_1:39; LIN c,c',b' by A3,A7,AFF_1:15;
     then b' in C by A3,AFF_1:39;
     hence contradiction by A3,A8,AFF_1:33; end;
     A9: a<>p proof assume a=p;
      then LIN a,c,q by A3,AFF_1:def 1;
      then LIN c,q,a & LIN c,q,b & LIN c,q,c by A3,AFF_1:15,16;
      hence contradiction by A3,A6,AFF_1:17; end;
     A10: a<>a' proof assume A11: a=a'; then LIN p,a,b & LIN p,a,b' &
      LIN p,a,a by A3,AFF_1:15,16; then LIN b,b',a by A9,AFF_1:17;
      then b=b' or a in P by A3,AFF_1:39;
      then LIN q,b,c & LIN q,b,c' & LIN q,b,b by A3,AFF_1:15,16,59
; then A12: q=b or
      LIN c,c',b by AFF_1:17;
        LIN a,c,c' by A3,A11,AFF_1:def 1; then LIN c,c',a
      by AFF_1:15; then A13: a in C by A3,AFF_1:39;
      then not b in C by A3,AFF_1:33;
      then LIN p,q,a by A3,A12,AFF_1:15,39; then p,q // p,a
      by AFF_1:def 1; then a,c // p,a by A3,AFF_1:14;
      then a,c // a,p by AFF_1:13; then LIN a,c,p by AFF_1:def 1;
      then p in C & LIN p,a,b by A3,A4,A13,AFF_1:15,39;
      then b in C by A3,A9,A13,AFF_1:39;
      hence contradiction by A3,A13,AFF_1:33; end;
     A14: b<>b' proof assume A15: b=b'; then LIN p,b,a & LIN p,b,a' &
      LIN p,b,b by A3,AFF_1:15,16; then p=b or LIN a,a',b by AFF_1:17;
      then A16: p=b or b in A by A3,A10,AFF_1:39;
        LIN q,b,c & LIN q,b,c' & LIN q,b,b by A3,A15,AFF_1:15,16;
      then b=q or LIN c,c',b by AFF_1:17; then A17: b in C by A3,A16,AFF_1:39,
59;
      then q in C & p in C & p,q // c,a by A3,A16,AFF_1:13,39,59;
      then a in C by A3,AFF_1:62; hence contradiction by A3,A17,AFF_1:33; end
;
     A18: A'<>P' proof assume A'=P'; then LIN p,a,c & LIN p,a,b &
      LIN p,a,a by A3,A5,AFF_1:15,33;
      hence contradiction by A3,A9,AFF_1:17; end;
     A19: A'<>C' proof assume A'=C'; then LIN a,a',c & LIN a,a',c'
      by A5,AFF_1:33; then c in A & c' in A by A3,A10,AFF_1:39;
      hence contradiction by A3,AFF_1:30; end;
     A20: P'<>C' proof assume P'=C'; then LIN p,a',c' & LIN p,a',b' &
      LIN p,a',a' by A3,A5,AFF_1:15,33;
      then p=a' by A3,AFF_1:17; then LIN a,a',b by A3,AFF_1:15;
      then b in A by A3,A10,AFF_1:39;
      hence contradiction by A3,AFF_1:59; end;
     A21: a',c' // p,q & a',c' // a,c by A3,A4,AFF_1:13,14;
     then A22: C' // P' & C' // A' & A' // P' by A3,A4,A5,AFF_1:52;
     A23: a',a // b',b by A3,A10,A14,AFF_1:52;
     A24: LIN p,a,b & LIN p,a',b' & LIN q,c,b & LIN q,c',b' by A3,AFF_1:15;
     A25: not LIN p,a',a proof assume LIN p,a',a; then LIN p,a,a' &
      LIN p,a,a by AFF_1:15,16; then LIN a,a',b by A9,A24,AFF_1:17;
      then b in A by A3,A10,AFF_1:39;
      hence contradiction by A3,AFF_1:59; end;
        not LIN q,c',c proof assume A26: LIN q,c',c; then LIN q,c,c' &
      LIN q,c,c by AFF_1:15,16; then LIN c,c',b by A6,A24,AFF_1:17;
      then A27: b in C by A3,AFF_1:39;
        LIN q,c',c' by AFF_1:16; then A28: LIN
 c,c',b' or q=c' by A24,A26,AFF_1:17;
        now assume q=c'; then c',a' // c',p by A21,AFF_1:13;
       then LIN c',a',p by AFF_1:def 1; then p in C' by A4,A5,AFF_1:39;
       then p=a' or b' in C' by A5,A24,AFF_1:39; then LIN a,a',b
       by A3,A5,AFF_1:15,33; then b in A by A3,A10,AFF_1:39;
      hence contradiction by A3,AFF_1:59; end;
      then b' in C by A3,A28,AFF_1:39;
      hence contradiction by A3,A14,A27,AFF_1:30; end;
     then a',a // c',c by A2,A5,A14,A18,A19,A20,A22,A23,A24,A25,Def6;
     hence A // C by A3,A10,AFF_1:52; end;
    hence thesis; end;
   end;

      AP satisfies_DES2_3 implies AP satisfies_DES2_1
    proof assume A29: AP satisfies_DES2_3;
    thus AP satisfies_DES2_1 proof let A,P,C,a,a',b,b',c,c',p,q;
    assume A30: A is_line & P is_line & C is_line &
     A<>P & A<>C & P<>C & a in A & a' in A & b in P & b' in P &
     c in C & c' in C & A // P & A // C & not LIN b,a,c &
     not LIN b',a',c' & p<>q & LIN b,a,p & LIN b',a',p & LIN b,c,q &
     LIN b',c',q & a,c // p,q;
    assume A31: not thesis;
    A32: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A30,AFF_1:16;
    set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
    A33: A' is_line & P' is_line & C' is_line & a in A' & c in A' &
     p in P' & q in P' & a' in C' & c' in C' by A30,A32,AFF_1:38;
    A34: C // A & C // P by A30,AFF_1:58;
    then A35: c,c' // a,a' & c,c' // b,b' by A30,AFF_1:53;
    A36: A' // P' by A30,A32,A33,AFF_1:52;
    A37: q<>c proof assume A38: q=c; then c,p // c,a by A30,AFF_1:13;
     then LIN c,p,a by AFF_1:def 1;
     then LIN p,a,c & LIN p,a,b & LIN p,a,a by A30,AFF_1:15,16;
     then a=p by A30,AFF_1:17; then LIN a,a',b' by A30,AFF_1:15;
then A39:     b' in A or a=a' by A30,AFF_1:39;
       LIN c,c',b' by A30,A38,AFF_1:15; then c =c' or b' in C by A30,AFF_1:39;
     hence contradiction by A30,A31,A34,A39,AFF_1:11,59; end;
    A40: a<>p proof assume a=p;
     then LIN a,c,q by A30,AFF_1:def 1;
     then LIN c,q,a & LIN c,q,b & LIN c,q,c by A30,AFF_1:15,16;
     hence contradiction by A30,A37,AFF_1:17; end;
    A41: a<>a' proof assume A42: a=a'; then LIN p,a,b & LIN p,a,b' &
     LIN p,a,a by A30,AFF_1:15,16; then LIN b,b',a by A40,AFF_1:17;
     then a in P or b=b' by A30,AFF_1:39;
     then LIN b,q,c & LIN b,q,c' & LIN b,q,b by A30,AFF_1:15,16,59;
     then b=q or LIN c,c',b by AFF_1:17;
     then b=q or c =c' or b in
 C by A30,AFF_1:39; then LIN p,q,a by A30,A31,A34,A42,AFF_1:11,15,59;
     then p,q // p,a by AFF_1:def 1; then a,c // p,a by A30,AFF_1:14;
     then a,c // a,p by AFF_1:13; then LIN a,c,p by AFF_1:def 1;
     then LIN p,a,c & LIN p,a,b & LIN p,a,a by A30,AFF_1:15,16;
     hence contradiction by A30,A40,AFF_1:17; end;
    A43: A'<>P' proof assume A'=P'; then LIN p,a,c & LIN p,a,b &
      LIN p,a,a by A30,A33,AFF_1:15,33;
      hence contradiction by A30,A40,AFF_1:17; end;
    A44: A'<>C' by A31,A33,AFF_1:65;
    A45: b<>b' proof assume b=b'; then LIN b,p,a & LIN b,p,a' &
     LIN b,p,b by A30,AFF_1:15,16; then b=p or LIN a,a',b by AFF_1:17;
     then A46: b=p or b in A by A30,A41,AFF_1:39;
     then LIN p,q,c by A30,AFF_1:15,59;
     then p,q // p,c by AFF_1:def 1;
     then a,c // p,c by A30,AFF_1:14; then c,a // c,p by AFF_1:13;
     then LIN c,a,p by AFF_1:def 1; hence contradiction by A30,A46,AFF_1:15,59
; end;
    A47: not LIN q,c,c' proof assume A48: LIN q,c,c'; LIN q,c,b &
     LIN q,c,c by A30,AFF_1:15,16; then LIN c,c',b by A37,A48,AFF_1:17;
     then c =c' or b in C by A30,AFF_1:39;
     then LIN q,c,b & LIN q,c,b' & LIN
 q,c,c by A30,A34,AFF_1:15,16,59
;
     then LIN b,b',c by A37,AFF_1:17; then c in P by A30,A45,AFF_1:39;
     hence contradiction by A30,A34,AFF_1:59; end;
    A49: not LIN p,a,a' proof assume LIN p,a,a'; then LIN p,a,a' &
     LIN p,a,b & LIN p,a,a by A30,AFF_1:15,16;
     then LIN a,a',b by A40,AFF_1:17; then b in A by A30,A41,AFF_1:39;
     hence contradiction by A30,AFF_1:59; end;
      LIN q,c,b & LIN q,c',b' & LIN p,a,b & LIN p,a',b' by A30,AFF_1:15;
    then A' // C' by A29,A32,A33,A35,A36,A43,A44,A45,A47,A49,Def8;
    hence contradiction by A31,A33,AFF_1:53;
    end;
   end;
  hence thesis by A1; end;

theorem
   AP satisfies_DES2 iff AP satisfies_DES2_2 proof
 A1: AP satisfies_DES2 implies AP satisfies_DES2_2
  proof assume A2: AP satisfies_DES2;
  thus AP satisfies_DES2_2 proof let A,P,C,a,a',b,b',c,c',p,q;
  assume A3: A is_line & P is_line & C is_line & A<>P &
   A<>C & P<>C & a in A & a' in A & b in P & b' in P & c in C &
   c' in C & A // C & not LIN b,a,c & not LIN b',a',c' & p<>q &
   a<>a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
   a,c // a',c' & a,c // p,q;
  then A4: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by AFF_1:16;
  A5: a<>p proof assume A6: a=p; then LIN a,a',b' by A3,AFF_1:15;
   then A7: b' in A by A3,AFF_1:39;
     LIN a,c,q by A3,A6,AFF_1:def 1;
   then LIN c,q,a & LIN c,q,b & LIN c,q,c by A3,AFF_1:15,16;
   then q=c by A3,AFF_1:17; then LIN c,c',b' by A3,AFF_1:15; then c =c' or
   b' in C by A3,AFF_1:39; then c,a // c,a' by A3,A7,AFF_1:13,59;
   then LIN c,a,a' by AFF_1:def 1; then LIN a,a',c by AFF_1:15; then c in A
by A3,AFF_1:39; hence contradiction by A3,AFF_1:59; end;
  A8: q<>c proof assume q=c; then c,p // c,a by A3,AFF_1:13;
   then LIN c,p,a by AFF_1:def 1; then LIN p,a,c & LIN p,a,b & LIN p,a,a by A3,
AFF_1:15,16; hence contradiction by A3,A5,AFF_1:17; end;
  A9: c <>c' proof assume c =c'; then c,a // c,a' by A3,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 A3,AFF_1:39; hence contradiction by A3,AFF_1:59; end;
  A10: a'<>p proof assume A11: a'=p; then LIN a,a',b by A3,AFF_1:15;
   then A12: b in A by A3,AFF_1:39; a',c' // p,q by A3,A4,AFF_1:14;
   then LIN a',c',q by A11,AFF_1:def 1; then LIN c',q,a' & LIN c',q,b' &
   LIN c',q,c' by A3,AFF_1:15,16; then q=c' by A3,AFF_1:17;
   then LIN c,c',b by A3,AFF_1:15; then b in C by A3,A9,AFF_1:39;
   hence contradiction by A3,A12,AFF_1:59; end;
  A13: c'<>q proof assume c'=q;
   then a',c' // p,c' by A3,A4,AFF_1:14; then c',a' // c',p by AFF_1:13;
   then LIN c',a',p by AFF_1:def 1; then LIN p,a',c' & LIN p,a',b' & LIN p,a'
,a' by A3,AFF_1:15,16; hence contradiction by A3,A10,AFF_1:17; end;
  A14: b<>b' proof assume b=b'; then LIN b,p,a & LIN b,p,a' &
   LIN b,p,b & LIN b,q,c & LIN b,q,c' & LIN b,q,b by A3,AFF_1:15,16;
   then (b=p or LIN a,a',b) & (b=q or LIN c,c',b) by AFF_1:17;
then A15:   (b=p or b in A) & (b=q or b in C) by A3,A9,AFF_1:39;
A16:   now assume A17: b=p & b in C; then LIN p,q,c & p in C by A3,AFF_1:15;
then p,q // p,c by AFF_1:def 1;
    then a,c // p,c by A3,AFF_1:14; then c,a // c,p by AFF_1:13;
    then LIN c,a,p by AFF_1:def 1;
    hence contradiction by A3,A17,AFF_1:15; end;
    then q in A & LIN q,p,a by A3,A15,AFF_1:15,59;
   then q in A & q,p // q,a by AFF_1:def 1; then q in A & p,q // q,a
   by AFF_1:13; then q in A & a,c // q,a by A3,AFF_1:14; then q in A &
   a,c // a,q by AFF_1:13; then q in A & LIN a,c,q by AFF_1:def 1;
   then q in A & LIN a,q,c by AFF_1:15; then c in A or a=q by A3,AFF_1:39;
   hence contradiction by A3,A15,A16,AFF_1:16,59; end;
  set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
  A18: A' is_line & P' is_line & C' is_line & a in A' & c in A' &
   p in P' & q in P' & a' in C' & c' in C' by A3,A4,AFF_1:38;
    a',c' // a,c & a',c' // p,q by A3,A4,AFF_1:13,14;
  then A19: C' // A' & C' // P' by A3,A4,A18,AFF_1:52;
  A20: C'<>A' proof assume C'=A'; then LIN a,a',c by A18,AFF_1:33;
   then c in A by A3,AFF_1:39;
   hence contradiction by A3,AFF_1:59; end;
  A21: C'<>P' proof assume C'=P'; then LIN p,a',c' & LIN p,a',b' &
   LIN p,a',a' by A3,A18,AFF_1:15,33;
   hence contradiction by A3,A10,AFF_1:17; end;
  A22: P'<>A' proof assume P'=A'; then LIN p,a,c & LIN p,a,b &
   LIN p,a,a by A3,A18,AFF_1:15,33;
   hence contradiction by A3,A5,AFF_1:17; end;
  A23: LIN p,a',b' & LIN p,a,b & LIN q,c',b' & LIN q,c,b by A3,AFF_1:15;
  A24: not LIN p,a',a proof assume LIN p,a',a; then LIN p,a',a &
   LIN p,a',a' & LIN p,a,a' & LIN p,a,a by AFF_1:15,16;
   then LIN a,a',b' & LIN a,a',b by A5,A10,A23,AFF_1:17;
   then b in A & b' in A by A3,AFF_1:39;
   hence contradiction by A3,A14,AFF_1:30; end;
  A25: not LIN q,c',c proof assume LIN q,c',c; then LIN q,c',c &
   LIN q,c',c' & LIN q,c,c' & LIN q,c,c by AFF_1:15,16;
   then LIN c,c',b & LIN c,c',b' by A8,A13,A23,AFF_1:17;
   then b in C & b' in C by A3,A9,AFF_1:39;
   hence contradiction by A3,A14,AFF_1:30; end;
    a',a // c',c by A3,AFF_1:53;
  then a',a // b',b by A2,A4,A14,A18,A19,A20,A21,A22,A23,A24,A25,Def5;
  hence A // P by A3,A14,AFF_1:52; end;
 end;
    AP satisfies_DES2_2 implies AP satisfies_DES2
 proof assume A26: AP satisfies_DES2_2;
 thus AP satisfies_DES2 proof let A,P,C,a,a',b,b',c,c',p,q;
 assume A27: A is_line & P is_line & C is_line & A<>P & A<>C &
  P<>C & a in A & a' in A & b in P & b' in P & c in C &
  c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' &
  p<>q & a<>a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
  a,c // a',c';
 then A28: C // P & C // A by AFF_1:58;
 A29: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A27,AFF_1:16;
 A30: c <>c' proof assume c =c'; then c,a // c,a' by A27,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 A27,AFF_1:39; hence contradiction by A27,AFF_1:59; end;
 A31: a<>p proof assume a=p; then LIN a,a',b' by A27,AFF_1:15; then b' in A
  by A27,AFF_1:39; hence contradiction by A27,AFF_1:59; end;
 A32: q<>c proof assume q=c; then LIN c,c',b' by A27,AFF_1:15; then b' in C
  by A27,A30,AFF_1:39; hence contradiction by A27,A28,AFF_1:59; end;
 A33: b<>b' proof assume b=b'; then LIN b,p,a & LIN b,p,a' &
   LIN b,p,b & LIN b,q,c & LIN b,q,c' & LIN
 b,q,b by A27,AFF_1:15,16;
   then (b=p or LIN a,a',b) & (b=q or LIN c,c',b) by AFF_1:17;
   then (b=p or b in A) & (b=q or b in C) by A27,A30,AFF_1:39;
   hence contradiction by A27,A28,AFF_1:59; end;
  set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
  A34: A' is_line & P' is_line & C' is_line & a in A' & c in A' &
   p in P' & q in P' & a' in C' & c' in C' by A27,A29,AFF_1:38;
  A35: c,c' // a,a' & c,c' // b,b' by A27,A28,AFF_1:53;
  A36: LIN q,c,b & LIN q,c',b' & LIN p,a,b & LIN p,a',b' by A27,AFF_1:15;
  A37: A' // C' by A27,A29,A34,AFF_1:52;
  A38: A'<>P' proof assume A'=P'; then LIN c,q,a & LIN c,q,b &
   LIN c,q,c by A27,A34,AFF_1:15,33;
   hence contradiction by A27,A32,AFF_1:17; end;
  A39: A'<>C' proof assume A'=C'; then LIN a,a',c by A34,AFF_1:33;
   then c in A by A27,AFF_1:39;
   hence contradiction by A27,AFF_1:59; end;
  A40: not LIN q,c,c' proof assume LIN q,c,c'; then LIN q,c,c' &
   LIN q,c,c by AFF_1:16; then LIN c,c',b by A32,A36,AFF_1:17; then b in C
by A27,A30,AFF_1:39; hence contradiction by A27,A28,AFF_1:59; end;
     not LIN p,a,a' proof assume LIN p,a,a'; then LIN p,a,a' &
   LIN p,a,a by AFF_1:16; then LIN a,a',b by A31,A36,AFF_1:17; then b in A
by A27,AFF_1:39; hence contradiction by A27,AFF_1:59; end;
  then A' // P' by A26,A29,A33,A34,A35,A36,A37,A38,A39,A40,Def7;
  hence thesis by A34,AFF_1:53; end;
 end;
 hence thesis by A1;
end;

theorem
   AP satisfies_DES1_3 implies AP satisfies_DES2_1
 proof assume A1: AP satisfies_DES1_3;
  let A,P,C,a,a',b,b',c,c',p,q such that
A2: A is_line and
A3: P is_line and
A4: C is_line and
A5: A<>P and
A6: A<>C and
A7: P<>C and
A8: a in A and
A9: a' in A and
A10: b in P and
A11: b' in P and
A12: c in C and
A13: c' in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b',a',c' and
A18: p<>q and
A19: LIN b,a,p and
A20: LIN b',a',p and
A21: LIN b,c,q and
A22: LIN b',c',q and
A23: a,c // p,q;
 assume A24: not thesis;
 A25: a<>b & b<>c & a<>c & a'<>b' & a'<>c' & b'<>c' by A16,A17,AFF_1:16;
 A26: P // C by A14,A15,AFF_1:58;
 A27: c <>q proof assume A28: c =q; then LIN c,c',b' by A22,AFF_1:15;
then A29:  c =c' or b' in C by A4,A12,A13,AFF_1:39;
    c,a // c,p by A23,A28,AFF_1:13; then LIN c,a,p by AFF_1:def 1;
  then LIN p,a,c & LIN p,a,b & LIN p,a,a by A19,AFF_1:15,16;
  then p=a by A16,AFF_1:17; then LIN a,a',b' by A20,AFF_1:15;
  then a=a' or b' in A by A2,A8,A9,AFF_1:39;
  hence contradiction by A5,A7,A11,A14,A24,A26,A29,AFF_1:11,59; end;
 A30: c <>c' proof assume A31: c =c'; then LIN q,c,b & LIN q,c,b' &
  LIN q,c,c by A21,A22,AFF_1:15,16; then LIN b,b',c by A27,AFF_1:17;
  then b=b' or c in P by A3,A10,A11,AFF_1:39;
  then LIN p,b,a' & LIN p,b,a & LIN p,b,b
      by A7,A12,A19,A20,A26,AFF_1:15,16,59;
  then A32: p=b or LIN a,a',b by AFF_1:17;
    now assume A33: p=b; then a,c // b,q & LIN b,q,c by A21,A23,AFF_1:15;
   then a,c // b,q & b,q // b,c by AFF_1:def 1; then a,c // b,c or
   b=q by AFF_1:14; then c,a // c,b by A18,A33,AFF_1:13; then LIN c,a,b
   by AFF_1:def 1; hence contradiction by A16,AFF_1:15; end; then a=a' or
  b in A by A2,A8,A9,A32,AFF_1:39;
  hence contradiction by A5,A10,A14,A24,A31,AFF_1:11,59; end;
 set K=Line(p,q), M=Line(a,c), N=Line(a',c');
 A34: K is_line & M is_line & N is_line & p in K &
  q in K & a in M & c in M & a' in N & c' in N
         by A18,A25,AFF_1:38; then A35: M // K by A18,A23,A25,AFF_1:52;
   not M // N by A24,A34,AFF_1:53; then consider
 x such that A36: x in M & x in N by A34,AFF_1:72;
   C // P & C // A by A14,A15,AFF_1:58;
 then A37: c,c' // b,b' & c,c' // a,a' by A8,A9,A10,A11,A12,A13,AFF_1:53;
 A38: LIN q,c,b & LIN q,c',b' & LIN p,a,b & LIN p,a',b'
    by A19,A20,A21,A22,AFF_1:15;
 A39: b<>b' proof assume b=b'; then LIN q,b,c & LIN q,b,c' &
  LIN q,b,b by A21,A22,AFF_1:15,16;
  then q=b or LIN c,c',b by AFF_1:17;
  then A40:  q=b or b in C by A4,A12,A13,A30,AFF_1:39;
  then a,c // p,b &
  b,a // b,p by A7,A10,A19,A23,A26,AFF_1:59,def 1;
  then a,c // p,b & a,b // p,b
  by AFF_1:13; then a,c // a,b or p=b by AFF_1:14; then LIN a,c,b by A7,A10,A18
,A26,A40,AFF_1:59,def 1;
   hence contradiction by A16,AFF_1:15;
  end;
 A41: p<>a proof assume p=a; then LIN a,c,q
  by A23,AFF_1:def 1; then LIN c,q,a & LIN c,q,b & LIN
 c,q,c by A21,AFF_1:15,16;
  hence contradiction by A16,A27,AFF_1:17; end;
  A42: now assume M=K; then LIN q,c,a & LIN q,c,b & LIN q,c,c by A21,A34,AFF_1:
15,33;
   hence contradiction by A16,A27,AFF_1:17; end;
 A43: M<>N by A24,A34,AFF_1:65;
  A44: now assume x=c; then N=C by A4,A12,A13,A30,A34,A36,AFF_1:30;
   hence contradiction by A6,A9,A15,A34,AFF_1:59; end;
A45: now assume x=c'; then M=C by A4,A12,A13,A30,A34,A36,AFF_1:30;
   hence contradiction by A6,A8,A15,A34,AFF_1:59; end;
 A46: not LIN q,c,c' proof assume LIN q,c,c'; then LIN q,c,c' & LIN q,c,b &
  LIN q,c,c by A21,AFF_1:15,16; then LIN c,c',b by A27,AFF_1:17;
  then b in C by A4,A12,A13,A30,AFF_1:39;
  hence contradiction by A7,A10,A26,AFF_1:59; end;
    not LIN p,a,a' proof assume LIN p,a,a'; then LIN p,a,a' &
  LIN p,a,b & LIN p,a,a by A19,AFF_1:15,16;
  then LIN a,a',b by A41,AFF_1:17; then a=a' or b in A by A2,A8,A9,AFF_1:39;
  then LIN p,a,b & LIN p,a,b' & LIN p,a,a
      by A5,A10,A14,A19,A20,AFF_1:15,16,59;
  then LIN b,b',a
  by A41,AFF_1:17; then a in P by A3,A10,A11,A39,AFF_1:39;
  hence contradiction by A5,A8,A14,AFF_1:59; end;
 then x in K by A1,A18,A25,A34,A36,A37,A38,A39,A43,A44,A45,A46,Def4;
 hence contradiction by A35,A36,A42,AFF_1:59;
end;

Back to top