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;