Copyright (c) 1990 Association of Mizar Users
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;