Copyright (c) 1990 Association of Mizar Users
environ
vocabulary DIRAF, AFF_1, ANALOAF, INCSP_1, AFF_2, AFF_3;
notation STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2;
constructors AFF_1, AFF_2, XBOOLE_0;
clusters ZFMISC_1, XBOOLE_0;
definitions AFF_2;
theorems AFF_1, AFF_2;
begin
reserve AP for AffinPlane;
reserve a,a',b,b',c,c',d,x,y,o,p,q
for Element of AP;
reserve A,C,D',M,N,P
for Subset of AP;
definition let AP;
attr AP is satisfying_DES1 means
:Def1: for A,P,C,o,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
o in A & a in A & a' in A & o in P & b in P & b' in P &
o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
not LIN b,a,c & not LIN b',a',c' & a<>a' &
LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' holds a,c // p,q;
synonym AP satisfies_DES1;
end;
definition let AP;
attr AP is satisfying_DES1_1 means
:Def2: for A,P,C,o,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
o in A & a in A & a' in A & o in P & b in P & b' in P &
o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
c <>q & not LIN b,a,c & not LIN b',a',c' &
LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // p,q holds a,c // a',c';
synonym AP satisfies_DES1_1;
end;
definition let AP;
attr AP is satisfying_DES1_2 means
:Def3: for A,P,C,o,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
o in A & a in A & a' in A & o in P & b in P & b' in P &
c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
not LIN b,a,c & not LIN b',a',c' & c <>c' &
LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' & a,c // p,q holds o in C;
synonym AP satisfies_DES1_2;
end;
definition let AP;
attr AP is satisfying_DES1_3 means
:Def4: for A,P,C,o,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
o in A & a in A & a' in A & b in P & b' in P &
o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
not LIN b,a,c & not LIN b',a',c' & b<>b' & a<>a' &
LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' & a,c // p,q holds o in P;
synonym AP satisfies_DES1_3;
end;
definition let AP;
attr AP is satisfying_DES2 means
:Def5: for A,P,C,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
a in A & a' in A & b in P & b' in P & c in C & c' in C &
A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p<>q &
a<>a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' holds a,c // p,q;
synonym AP satisfies_DES2;
end;
definition let AP;
attr AP is satisfying_DES2_1 means
:Def6: for A,P,C,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
a in A & a' in A & b in P & b' in P & c in C & c' in C &
A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p<>q &
LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // p,q holds a,c // a',c';
synonym AP satisfies_DES2_1;
end;
definition let AP;
attr AP is satisfying_DES2_2 means
:Def7: for A,P,C,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
a in A & a' in A & b in P & b' in P & c in C & c' in C &
A // C & not LIN b,a,c & not LIN b',a',c' & p<>q & a<>a' &
LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' & a,c // p,q holds A // P;
synonym AP satisfies_DES2_2;
end;
definition let AP;
attr AP is satisfying_DES2_3 means
:Def8: for A,P,C,a,a',b,b',c,c',p,q st
A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
a in A & a' in A & b in P & b' in P & c in C & c' in C &
A // P & not LIN b,a,c & not LIN b',a',c' & p<>q & c <>c' &
LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' & a,c // p,q holds A // C;
synonym AP satisfies_DES2_3;
end;
canceled 8;
theorem
AP satisfies_DES1 implies AP satisfies_DES1_1
proof assume A1: AP satisfies_DES1;
let A,P,C,o,a,a',b,b',c,c',p,q;
assume that A2: A is_line & P is_line & C is_line and
A3: P<>A & P<>C & A<>C and
A4: o in A & a in A & a' in A & o in P & b in P &
b' in P & o in C & c in C & c' in C & o<>a & o<>b & o<>c
& p<>q & c <>q & not LIN b,a,c & not LIN b',a',c' and
A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q;
set K=Line(b,a); set M=Line(b,c);
b<>a & b<>c & a<>c by A4,AFF_1:16;
then A6: K is_line & M is_line & b in K & a in K & b in M & c in M &
p in K & q in M by A5,AFF_1:26,def 2,def 3;
A7: a'<>b' & b'<>c' & a'<>c' by A4,AFF_1:16;
A8: M<>P & K<>P by A2,A3,A4,A6,AFF_1:30;
A9: b<>o & b<>a & b<>c by A4,AFF_1:16;
A10: K<>M by A4,A6,AFF_1:33;
A11: not LIN o,a,c proof assume LIN o,a,c; then c in A
by A2,A4,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
p<>b by A4,A5,AFF_1:69;
then A12: p<>b' by A2,A4,A6,A8,AFF_1:30;
q<>b proof assume A13: q=b;
not LIN b,c,a & c,a // q,p & LIN b,c,q & LIN b,a,p by A4,A5,AFF_1:13,15;
hence contradiction by A4,A13,AFF_1:69; end;
then A14: q<>b' by A2,A4,A6,A8,AFF_1:30;
A15: not LIN b',p,q proof assume LIN b',p,q; then A16: LIN p,q,b'
by AFF_1:15; set N=Line(p,q);
A17: N is_line & p in N & q in N & b' in N
by A4,A16,AFF_1:26,def 2,def 3;
LIN p,b',a' & LIN q,b',c' by A5,AFF_1:15;
then a' in N & c' in N by A12,A14,A17,AFF_1:39;hence contradiction by A4,
A17,AFF_1:33; end;
A18: a <> p by A4,A5,AFF_1:23;
LIN o,a,a' & LIN b',p,a' & LIN o,c,c' & LIN b',q,c'
by A2,A4,A5,AFF_1:15,33;
hence thesis by A1,A2,A4,A5,A6,A7,A8,A9,A10,A11,A15,A18,Def1;
end;
theorem
AP satisfies_DES1_1 implies AP satisfies_DES1
proof assume A1: AP satisfies_DES1_1;
let A,P,C,o,a,a',b,b',c,c',p,q;
assume that A2: A is_line & P is_line & C is_line and
A3: P<>A & P<>C & A<>C and
A4: o in A & a in A & a' in A & o in P & b in P & b' in P &
o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
not LIN b,a,c & not LIN b',a',c' & a<>a' and
A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c'; set K=Line(b,a); set M=Line(b,c);
b<>a & b<>c & a<>c by A4,AFF_1:16;
then A6: K is_line & M is_line & b in K & a in K & b in M & c in M &
p in K & q in M by A5,AFF_1:26,def 2,def 3;
A7: a'<>b' & b'<>c' & a'<>c' by A4,AFF_1:16;
A8: K<>P by A2,A3,A4,A6,AFF_1:30;
A9: M<>P by A2,A3,A4,A6,AFF_1:30;
A10: M<>P & K<>P by A2,A3,A4,A6,AFF_1:30;
A11: b<>o & b<>a & b<>c by A4,AFF_1:16;
A12: K<>M by A4,A6,AFF_1:33;
A13: not LIN o,a,c proof assume LIN o,a,c; then c in A
by A2,A4,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
A14: c <>c' proof assume c =c';
then c,a // c,a' & LIN o,a,a' & not LIN o,c,a
by A2,A4,A5,A13,AFF_1:13,15,33;
hence contradiction by A4,AFF_1:23; end;
A15: now assume A16: not LIN b',p,q;
LIN o,a,a' & LIN b',p,a' & LIN o,c,c' & LIN b',q,c'
by A2,A4,A5,AFF_1:15,33;
hence thesis by A1,A2,A4,A5,A6,A7,A10,A11,A12,A13,A14,A16,Def2; end;
now assume A17: LIN b',p,q; set A'=Line(b',a'); set C'=Line(b',c');
A18: LIN b',q,p by A17,AFF_1:15;
A19: A' is_line & C' is_line & b' in A' & a' in A' & p in A' &
b' in C' & c' in C' & q in C' by A5,A7,AFF_1:26,def 2,def 3;
then A20: A'<>C' by A4,AFF_1:33;
A21: now assume b'<>p; then A22: q in A' by A17,A19,AFF_1:39;
then A23: q=b' by A19,A20,AFF_1:30; LIN
b,c,b' by A5,A19,A20,A22,AFF_1:30;
then b' in M
by AFF_1:def 2; then A24: b=b' by A2,A4,A6,A9,AFF_1:30;
A'<>K proof assume A'=K; then LIN a,a',b by A6,A19,AFF_1:33;
then b in A by A2,A4,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
then p=q by A6,A19,A23,A24,AFF_1:30;
hence thesis by AFF_1:12; end;
now assume b'<>q; then A25: p in C' by A18,A19,AFF_1:39;
then A26: p=b' by A19,A20,AFF_1:30; LIN b,a,b' by A5,A19,A20,A25,AFF_1:30
;
then b' in K
by AFF_1:def 2; then A27: b=b' by A2,A4,A6,A8,AFF_1:30;
C'<>M proof assume C'=M; then LIN c,c',b by A6,A19,AFF_1:33;
then b in C by A2,A4,A14,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
then p=q by A6,A19,A26,A27,AFF_1:30;
hence thesis by AFF_1:12; end;
hence thesis by A4,A21; end;
hence thesis by A15;
end;
theorem
AP satisfies_DES implies AP satisfies_DES1
proof assume A1: AP satisfies_DES;
let A,P,C,o,a,a',b,b',c,c',p,q;
assume that A2: A is_line & P is_line & C is_line and
A3: P<>A & P<>C & A<>C and
A4: o in A & a in A & a' in A & o in P & b in P & b' in P &
o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
not LIN b,a,c & not LIN b',a',c' & a<>a' and
A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c';
set K=Line(b',a'); set M=Line(b',c');
A6: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A4,AFF_1:16;
then A7: K is_line & M is_line & b' in K & a' in K & p in K &
b' in M & c' in M & q in M by A5,AFF_1:26,def 2,def 3;
A8: not LIN o,a,c proof assume LIN o,a,c; then c in A
by A2,A4,AFF_1:39; hence
contradiction by A2,A3,A4,AFF_1:30; end;
A9: o<>a' proof assume A10: o=a';
LIN o,a,a' & LIN o,c,c' by A2,A4,AFF_1:33;
hence
contradiction by A5,A6,A8,A10,AFF_1:69; end;
A11: o<>c' proof assume A12: o=c';
LIN o,a,a' & LIN o,c,c' & c,a // c',a' & not LIN o,c,a
by A2,A4,A5,A8,AFF_1:13,15,33;
hence contradiction by A9,A12,AFF_1:69; end;
A13: c <>c' proof assume c =c';
then LIN o,a,a' & c,a // c,a' & not LIN o,c,a
by A2,A4,A5,A8,AFF_1:13,15,33;
hence contradiction by A4,AFF_1:23; end;
A14: K<>P & M<>P & K<>M by A2,A3,A4,A7,A9,A11,AFF_1:30,33;
set D=Line(b,c); A15: D is_line & b in D & c in D & q in D
by A5,A6,AFF_1:26,def 2,def 3;
then consider D' such that A16: c' in D' & D // D' by AFF_1:63;
A17: D' is_line & D' // D by A16,AFF_1:50;
not D' // P proof assume D' // P; then D // P
by A16,AFF_1:58; then c in P
by A4,A15,AFF_1:59; hence
contradiction by A2,A3,A4,AFF_1:30; end; then consider d such that
A18: d in D' & d in P by A2,A17,AFF_1:72;
A19: d<>b' proof assume d=b'; then M=D'
by A6,A7,A16,A17,A18,AFF_1:30; then D=M
by A7,A15,A16,AFF_1:59; then LIN c,c',b by A7,A15,AFF_1:33;
then b in C by A2,A4,A13,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
c,b // c',d & c,a // c',a' by A5,A15,A16,A18,AFF_1:13,53;
then A20: b,a // d,a' by A1,A2,A3,A4,A18,AFF_2:def 4;
b,a // b,p by A5,AFF_1:def 1;
then d,a' // b,p & b,q // d,c' by A6,A15,A16,A18,A20,AFF_1:14,53;
then d,a' // b,p & d,c' // b,q by AFF_1:13;
then a',c' // p,q by A1,A2,A4,A6,A7,A14,A18,A19,AFF_2:def 4;
hence thesis by A5,A6,AFF_1:14;
end;
theorem
AP satisfies_DES implies AP satisfies_DES1_2
proof assume A1: AP satisfies_DES;
then A2: AP satisfies_DES_1 by AFF_2:16;
let A,P,C,o,a,a',b,b',c,c',p,q;
assume that A3: A is_line & P is_line & C is_line and
A4: P<>A & P<>C & A<>C and
A5: o in A & a in A & a' in A & o in P & b in P &
b' in P & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
not LIN b,a,c & not LIN b',a',c' & c <>c' and
A6: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' & a,c // p,q;
A7: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A5,AFF_1:16;
A8: b'<>a' & b'<>c' by A5,AFF_1:16;
set K=Line(b',a'); set M=Line(b',c');
A9: K is_line & M is_line & b' in K & a' in K & p in K &
b' in M & c' in M & q in M by A6,A7,AFF_1:26,def 2,def 3;
then A10: K<>M by A5,AFF_1:33;
A11: b<>q proof assume A12: b=q; not LIN b,c,a & c,a // q,p
by A5,A6,AFF_1:13,15;
hence contradiction by A5,A6,A12,AFF_1:69; end;
A13: b'<>q proof assume A14: b'=q; a',c' // p,q by A6,A7,AFF_1:14;
then c',a' // q,p & not LIN b',c',a' by A5,AFF_1:13,15;hence
contradiction by A5,A6,A14,AFF_1:69; end;
A15: b'<>p proof assume A16: b'=p; a',c' // p,q by A6,A7,AFF_1:14;
hence
contradiction by A5,A6,A16,AFF_1:69; end;
A17: b<>p by A5,A6,AFF_1:69;
now
A18: now assume A19: M=P;
LIN b,q,c by A6,AFF_1:15; then c in P by A5,A9,A11,A19,AFF_1:39;
then P=Line(c,c') by A5,A9,A19,AFF_1:71;
hence thesis by A3,A5,AFF_1:71; end;
now assume A20: M<>P; set D=Line(b,c);
A21: D is_line & b in D & c in D & q in D
by A6,A7,AFF_1:26,def 2,def 3; then consider D' such that
A22: c' in D' & D // D' by AFF_1:63;
A23: D' is_line by A22,AFF_1:50;
not D' // P proof assume D' // P; then D // P
by A22,AFF_1:58; then q in P
by A5,A21,AFF_1:59; hence
contradiction by A3,A5,A9,A13,A20,AFF_1:30
; end; then consider d such that
A24: d in D' & d in P by A3,A23,AFF_1:72;
A25: q,b // c',d & b,c // d,c' by A21,A22,A24,AFF_1:53;
then A26: c',d // q,b & b,c // d,c' by AFF_1:13;
A27: d<>b' proof assume d=b';
then M=D' by A7,A9,A22,A23,A24,AFF_1:30;
then D=M by A9,A21,A22,AFF_1:59;
then LIN c,c',b & LIN c,c',b' by A9,A21,AFF_1:33; then A28: b in C &
b' in C by A3,A5,AFF_1:39;
set T=Line(b,a); set N=Line(a,c);
A29: T is_line & b in T & a in T & p in T
by A6,A7,AFF_1:26,def 2,def 3;
A30: N is_line & a in N & c in N by A7,AFF_1:26,def 3;
A31: a<>a' proof assume a=a'; then LIN a,c,c'
by A6,AFF_1:def 1;
then c' in N
by AFF_1:def 2; then N=C by A3,A5,A30,AFF_1:30;
hence contradiction by A5,A28,A30,AFF_1:33; end;
b<>b' proof assume A32: b=b';
K<>T proof assume K=T; then T=A by A3,A5,A9,A29,A31,AFF_1:30;
hence
contradiction by A3,A4,A5,A29,AFF_1:30; end;
hence contradiction by A9,A15,A29,A32,AFF_1:30; end;
hence contradiction by A3,A4,A5,A28,AFF_1:30; end;
p,q // a',c' by A6,A7,AFF_1:14; then c',a' // q,p by AFF_1:13;
then A33: d,a' // b,p by A1,A3,A5,A8,A9,A10,A20,A24,A26,A27,AFF_2:def 4;
b,a // b,p by A6,AFF_1:def 1;
then b,a // d,a' by A17,A33,AFF_1:14;
hence thesis by A2,A3,A4,A5,A6,A24,A25,AFF_2:def 5; end;
hence thesis by A18; end;
hence thesis;
end;
theorem
AP satisfies_DES1_2 implies AP satisfies_DES1_3
proof assume A1: AP satisfies_DES1_2;
let A,P,C,o,a,a',b,b',c,c',p,q;
assume that A2:A is_line & P is_line & C is_line and
A3: P<>A & P<>C & A<>C and
A4: o in A & a in A & a' in A & b in P & b' in P &
o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
not LIN b,a,c & not LIN b',a',c' & b<>b' & a<>a' and
A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' & a,c // p,q;
assume A6: not thesis;
A7: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A4,AFF_1:16;
A8: not LIN o,c,a proof assume LIN o,c,a; then a in C
by A2,A4,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
A9: c <>c' proof assume c =c';
then LIN o,a,a' & c,a // c,a' by A2,A4,A5,AFF_1:13,33;
hence contradiction by A4,A8,AFF_1:23; end;
A10: a',c' // p,q by A5,A7,AFF_1:14;
A11: p<>b & p<>b' & q<>b & q<>b' proof assume A12: not thesis;
A13: now assume A14: b=q; not LIN b,c,a & c,a // q,p
by A4,A5,AFF_1:13,15; hence
contradiction by A4,A5,A14,AFF_1:69; end;
now assume A15: b'=q; not LIN b',c',a' & c',a' // q,p
by A4,A10,AFF_1:13,15; hence
contradiction by A4,A5,A15,AFF_1:69; end;
hence contradiction by A4,A5,A10,A12,A13,AFF_1:69; end;
A16: not P // A or not C // P proof assume not thesis;
then C // A by AFF_1:58; hence
contradiction by A3,A4,AFF_1:59; end;
set D=Line(b,c), T=Line(b,a), N=Line(p,q), M=Line(a',c'), K=Line(b',a');
A17: D is_line & T is_line & N is_line & M is_line &
K is_line & p in N & q in N & b in D & c in D &
b in T & a in T & a' in M & c' in M & b' in K &
a' in K by A4,A7,AFF_1:38;
then A18: q in D & p in T & p in K by A5,A7,AFF_1:39;
A19: now assume not P // A; then consider x such that
A20: x in P & x in A by A2,AFF_1:72;
A21: x<>a proof assume A22: x=a;
then A23: p in P & a in P by A2,A4,A5,A7,A20,AFF_1:39;
K<>P by A2,A3,A4,A17,A20,A22,AFF_1:30;
hence contradiction by A2,A4,A11,A17,A18,A23,AFF_1:30; end;
x<>b proof assume A24: x=b;
then LIN b,a,a' & LIN b,a,a by A2,A4,A20,AFF_1:33; then LIN a,a',p
by A5,A7,AFF_1:17; then p in A by A2,A4,AFF_1:39;
then a',c' // a',q or b' in A by A2,A4,A10,A17,A18,AFF_1:30
; then LIN a',c',q by A2,A3,A4,A20,A24,AFF_1:30,def 1;
then LIN q,c',a' & LIN q,c',b' & LIN q,c',c' by A5,AFF_1:15,16;
then q=c' by A4,AFF_1:17; then LIN c,c',b by A5,AFF_1:15; then b in C
by A2,A4,A9,AFF_1:39;
hence contradiction by A2,A3,A4,A20,A24,AFF_1:30; end;
then x in C by A1,A2,A3,A4,A5,A9,A20,A21,Def3;
hence contradiction by A2,A3,A4,A6,A20,AFF_1:30; end;
now assume not C // P; then consider x such that
A25: x in C & x in P by A2,AFF_1:72;
A26: x<>c proof assume A27: x=c;
then LIN b,c,b' & LIN b,c,c by A2,A4,A25,AFF_1:33; then LIN q,b',c &
LIN q,b',c' & LIN q,b',b' by A5,A7,AFF_1:15,17; then LIN c,c',b'
by A11,AFF_1:17; then A28: b' in C by A2,A4,A9,AFF_1:39;
then A29: c =b' by A2,A3,A4,A25,A27,AFF_1:30; LIN c,c',q by A2,A3,A4,A5,
A25,A27,A28,AFF_1:30;
then q in C by A2,A4,A9,AFF_1:39; then C=D by A2,A4,A11,A17,A18,A29,AFF_1:
30;
hence contradiction by A2,A3,A4,A17,A28,AFF_1:30; end;
A30: x<>b proof assume A31: x=b;
then LIN b,c,c' & LIN b,c,c by A2,A4,A25,AFF_1:33;
then LIN c,c',q by A5,A7,AFF_1:17;
then q in C & LIN q,c',b' by A2,A4,A5,A9,AFF_1:15,39;
then q=c' or b' in C by A2,A4,AFF_1:39; then c',a' // c',p
by A2,A3,A4,A10,A25,A31,AFF_1:13,30; then LIN c',a',p by AFF_1:def 1;
then LIN p,a',c' & LIN p,a',b' & LIN p,a',a' by A5,AFF_1:15,16;
then p=a' by A4,AFF_1:17; then LIN a,a',b by A5,AFF_1:15; then b in A
by A2,A4,AFF_1:39; hence contradiction by A2,A3,A4,A25,A31,AFF_1:30; end;
A32: not LIN b,c,a & not LIN b',c',a' by A4,AFF_1:15;
c,a // q,p & c,a // c',a' by A5,AFF_1:13;
then x in A by A1,A2,A3,A4,A5,A25,A26,A30,A32,Def3;
hence contradiction by A2,A3,A4,A6,A25,AFF_1:30; end;
hence contradiction by A16,A19;
end;
theorem
AP satisfies_DES1_2 implies AP satisfies_DES
proof assume A1: AP satisfies_DES1_2;
let A,P,C,o,a,b,c,a',b',c';
assume that A2: o in A & o in P & o in C & o<>a & o<>b & o<>c &
a in A & a' in A & b in P & b' in P & c in C & c' in C and
A3: A is_line & P is_line & C is_line and
A4: A<>P & A<>C and A5: a,b // a',b' & a,c // a',c';
now assume A6: P<>C;
then A7: a<>b & a<>c & b<>c by A2,A3,A4,AFF_1:30;
A8: not LIN o,b,a & not LIN o,a,c proof assume A9: not thesis;
A10: now assume LIN o,b,a; then a in P by A2,A3,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
now assume LIN o,a,c; then c in A by A2,A3,AFF_1:39;
hence contradiction by A2,A3,A4,AFF_1:30; end;
hence thesis by A9,A10; end;
A11: a'=o implies thesis proof assume A12: a'=o;
LIN o,a,a' & LIN o,c,c' & not LIN o,a,c by A2,A3,A8,AFF_1:33;
then A13: o=c' by A5,A12,AFF_1:69;
LIN o,a,a' & LIN o,b,b' & not LIN o,a,b by A2,A3,A8,AFF_1:15,33;
then o=b' by A5,A12,AFF_1:69;
hence thesis by A13,AFF_1:12; end;
A14: b'=o implies thesis proof assume A15: b'=o;
LIN o,b,b' & LIN o,a,a' & not LIN o,b,a & b,a // b',a'
by A2,A3,A5,A8,AFF_1:13,33;
hence thesis by A11,A15,AFF_1:69; end;
A16: c'=o implies thesis proof assume A17: c'=o;
LIN o,c,c' & LIN o,a,a' & not LIN o,c,a & c,a // c',a'
by A2,A3,A5,A8,AFF_1:13,15,33;
hence thesis by A11,A17,AFF_1:69; end;
set K=Line(a,c);
A18: K is_line & a in K & c in K by A7,AFF_1:26,def 3;
A19: LIN a,b,c implies thesis proof assume LIN a,b,c;
then LIN a,c,b by AFF_1:15; then A20: b in K by AFF_1:def 2;
then K=Line(a,b) & K=Line(b,c) by A7,A18,AFF_1:71;
then a,c // K & a,b // K by A7,AFF_1:43;
then A21: a',c' // K & a',b' // K by A5,A7,AFF_1:46;
consider N such that A22: a' in N & K // N by A18,AFF_1:63;
A23: N is_line by A22,AFF_1:50;
a',c' // N & a',b' // N by A21,A22,AFF_1:57;
then c' in N & b' in N by A22,A23,AFF_1:37;hence thesis by A18,A20,A22,
AFF_1:53; end;
A24: b=b' implies thesis proof assume A25: b=b';
then LIN o,a,a' & not LIN o,b,a & b,a // b,a'
by A2,A3,A5,A8,AFF_1:13,33;
then LIN o,c,c' & not LIN o,a,c & a,c // a,c'
by A2,A3,A5,A8,AFF_1:23,33; then c =c' by AFF_1:23;
hence thesis by A25,AFF_1:11; end;
now assume
A26: o<>a' & o<>b' & o<>c' & b<>b' & not LIN a,b,c;
then A27: a'<>b' & a'<>c' & b'<>c' by A2,A3,A4,A6,AFF_1:30;
assume not b,c // b',c'; then consider q such that
A28: LIN b,c,q & LIN b',c',q by AFF_1:74; consider M such that
A29: q in M & K // M by A18,AFF_1:63;
A30: M is_line by A29,AFF_1:50;
not a,b // M proof assume a,b // M;
then a,b // K by A29,AFF_1:57;
then b in K by A18,AFF_1:37;hence contradiction by A18,A26,AFF_1:33;
end;
then consider p such that
A31: p in M & LIN a,b,p by A30,AFF_1:73;
set N=Line(a',c');
A32: N is_line & a' in N & c' in N by A27,AFF_1:26,def 3;
A33: K // N by A5,A7,A27,AFF_1:51;
then A34: N // M by A29,AFF_1:58;
A35: not LIN a',b',c' proof assume LIN a',b',c';
then LIN a',c',b' by AFF_1:15; then b' in N by AFF_1:def 2; then a',b'
// N
by A32,AFF_1:37; then A36: a',b' // K by A33,AFF_1:57;
a',b' // a,b by A5,AFF_1:13; then a,b // K by A27,A36,AFF_1:46;
then b in K by A18,AFF_1:37;
hence contradiction by A18,A26,AFF_1:33; end;
A37: a<>a' proof assume a=a';
then not LIN o,a,b & LIN o,b,b' & a,b // a,b' by A2,A3,A5,A8,AFF_1:15,33;
hence contradiction by A26,AFF_1:23; end;
A38: c <>c' proof assume c =c'; then not LIN o,c,a & LIN o,a,a' &
c,a // c,a' by A2,A3,A5,A8,AFF_1:13,15,33;
hence contradiction by A37,AFF_1:23; end;
A39: A<>K by A2,A3,A4,A18,AFF_1:30;
not b',p // N proof assume b',p // N; then b',p // M
by A34,AFF_1:57; then p,b' // M by AFF_1:48;
then A40: b' in M by A30,A31,AFF_1:37;
A41: now assume b'=q; then LIN b,b',c
by A28,AFF_1:15; then c in
P by A2,A3,A26,AFF_1:39;hence contradiction by A2,A3,A6,AFF_1:30; end;
now assume A42: b'<>q; LIN b',q,c' by A28,AFF_1:15; then c' in M
by A29,A30,A40,A42,AFF_1:39;
then a' in N & b' in N & c' in
N by A32,A34,A40,AFF_1:59;hence contradiction by A32,A35,AFF_1:33; end;
hence thesis by A41; end; then consider x such that
A43: x in N & LIN b',p,x by A32,AFF_1:73;
A44: LIN b',x,p by A43,AFF_1:15;
A45: x<>a proof assume x=a;
then a in K & a' in K by A18,A32,A33,A43,AFF_1:59;
then A=K by A2,A3,A18,A37,AFF_1:30;
hence contradiction by A2,A3,A4,A18,AFF_1:30; end;
set A'=Line(x,a);
A46: A' is_line & x in A' & a in A' by A45,AFF_1:26,def 3;
A47: p<>q proof assume A48: p=q; then LIN p,b,c & LIN p,b,a &
LIN p,b,b by A28,A31,AFF_1:15,16; then p=b by A26,AFF_1:17;
then LIN b,b',c' by A28,A48,AFF_1:15; then c' in P by A2,A3,A26,AFF_1:39
;
hence contradiction by A2,A3,A6,A26,AFF_1:30; end;
A49: not LIN b',c',x proof assume LIN b',c',x;
then A50: LIN c',x,b' & LIN c',x,a' & LIN c',x,c'
by A32,A43,AFF_1:15,33;
then A51: c'=x or LIN b',c',a' by AFF_1:17;
A52: now assume c'=x; then LIN b',c',p & LIN b',c',c'
by A43,AFF_1:15,16;
then LIN p,q,c' by A27,A28,AFF_1:17; then c' in M by A29,A30,A31,A47,
AFF_1:39;
then q in N & LIN q,c',b' by A28,A29,A32,A34,AFF_1:15,59
; then A53: q=c' or b' in N
by A32,AFF_1:39;
now assume q=c'; then LIN c,c',b by A28,AFF_1:15; then b in C by A2,A3,
A38,AFF_1:39; hence contradiction by A2,A3,A6,AFF_1:30; end;
hence LIN b',c',a' by A32,A53,AFF_1:33; end;
then b',c' // b',a' by A51,AFF_1:def 1;
then b',c' // a',b' by AFF_1:13; then A54: b',c' // a,b by A5,A27,AFF_1:14
; LIN c',a',b' by A50,A52,AFF_1:15,17;
then c',a' // c',b' by AFF_1:def 1; then a',c' // b',c' by AFF_1:13;
then a,c // b',c' by A5,A27,AFF_1:14;
then a,c // a,b by A27,A54,AFF_1:14; then LIN a,c,b by AFF_1:def 1;
hence contradiction by A26,AFF_1:15; end;
A55: c,a // c',x by A18,A32,A33,A43,AFF_1:53;
A56: c,a // q,p by A18,A29,A31,AFF_1:53;
not LIN b,c,a & LIN b,a,p by A26,A31,AFF_1:15;
then o in A' by A1,A2,A3,A6,A28,A44,A45,A46,A47,A49,A55,A56,Def3;
then A57: x in A by A2,A3,A46,AFF_1:30;
A <> N by A2,A18,A33,A39,AFF_1:59;
then A58: x=a' by A2,A3,A32,A43,A57,AFF_1:30;
set D=Line(b,a); set T=Line(b',a');
A59: D is_line & T is_line & b in D & a in D & p in D &
b' in T & a' in T & p in T
by A7,A27,A31,A44,A58,AFF_1:26,def 2,def 3;
D // T by A5,A7,A27,AFF_1:51;
then a in D & a' in D by A59,AFF_1:59; then b in A by A2,A3,A37,A59,AFF_1:30;
hence contradiction by A2,A3,A4,AFF_1:30;
end;
hence thesis by A11,A14,A16,A19,A24; end;
hence thesis by A2,A3,AFF_1:65;
end;
theorem
AP satisfies_DES2_1 implies AP satisfies_DES2
proof assume A1: AP satisfies_DES2_1;
let A,P,C,a,a',b,b',c,c',p,q;
assume that A2: A is_line & P is_line & C is_line and
A3: A<>P & A<>C & P<>C and
A4: a in A & a' in A & b in P & b' in P & c in C & c' in C &
A // P & A // C & not LIN b,a,c & not LIN b',a',c' &
p<>q & a<>a'
and A5: LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c';
A6: P // C by A4,AFF_1:58;
A7: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A4,AFF_1:16;
set K=Line(a,c), N=Line(a',c'), D=Line(b,c), T=Line(b',c');
A8: K is_line & N is_line & D is_line & T is_line &
a in K & c in K & a' in N & c' in N & b in D &
c in D & q in D & b' in T & c' in T & q in T
by A5,A7,AFF_1:26,def 2,def 3;
A9: K // N by A5,A7,AFF_1:51;
A10: K<>A by A3,A4,A8,AFF_1:59;
A11: c <>c' proof assume c =c';
then K=N by A8,A9,AFF_1:59;hence contradiction by A2,A4,A8,A10,AFF_1:30
; end;
A12: D<>T proof assume D=T; then D=C by A2,A4,A8,A11,AFF_1:30;hence
contradiction by A3,A4,A6,A8,AFF_1:59; end;
set A'=Line(b,a); set P'=Line(b',a'); A13: A' is_line & P' is_line &
b in A' & a in A' & p in A' & b' in P' & a' in P' & p in P'
by A5,A7,AFF_1:26,def 2,def 3;
A14: b<>b' proof assume A15: b=b';
then A16: b'=q by A8,A12,AFF_1:30;
A'<>P' proof assume A'=P';
then A'=A by A2,A4,A13,AFF_1:30;hence contradiction by A3,A4,A13,AFF_1:59
; end;
hence contradiction by A4,A13,A15,A16,AFF_1:30; end;
consider M such that
A17: p in M & N // M by A8,AFF_1:63; A18: M is_line by A17,AFF_1:50;
A19: K // M by A9,A17,AFF_1:58;
A20: not M // D or not T // M proof assume not thesis;
then T // D by AFF_1:58; hence
contradiction by A8,A12,AFF_1:59; end;
A21: now assume not M // D; then consider x such that
A22: x in M & x in D by A8,A18,AFF_1:72;
not b',x // C proof assume A23: b',x // C;
C // P by A4,AFF_1:58; then b',x // P by A23,AFF_1:57; then x in P by A2,A4
,AFF_1:37;
then x=b or D=P by A2,A4,A8,A22,AFF_1:30;
then A24: b=p or M=A'
by A3,A4,A6,A8,A13,A17,A18,A22,AFF_1:30,59;
now assume b=p; then LIN b,b',a' by A13,AFF_1:33; then a' in P
by A2,A4,A14,AFF_1:39;
hence contradiction by A3,A4,AFF_1:59; end;
then b in K by A8,A13,A19,A24,AFF_1:59
; hence contradiction by A4,A8,AFF_1:33; end;
then consider y such that
A25: y in C & LIN b',x,y by A2,AFF_1:73;
A26: LIN b',y,x & LIN b,c,x & a,c // p,x
by A8,A17,A19,A22,A25,AFF_1:15,33,53;
A27: not LIN b',a',y proof assume LIN b',a',y;
then LIN b',y,a' & LIN b',y,b' by AFF_1:15,16; then b'=y or
LIN a',b',x by A26,AFF_1:17; then x in P' by A3,A4,A6,A25,AFF_1:59,def 2;
then A28: x=p or P'=M by A13,A17,A18,A22,AFF_1:30;
now assume x=p; then p=b or D=A'
by A8,A13,A22,AFF_1:30; then LIN
b,b',a' or c in A' by A13,AFF_1:26,33;
then a' in P by A2,A4,A14,AFF_1:39,def 2;
hence contradiction by A3,A4,AFF_1:59; end; then N=P' by A8,A13,A17,A28,
AFF_1:59
;hence contradiction by A4,A8,AFF_1:def 2; end;
p<>x proof assume p=x; then p=b or D=A'
by A8,A13,A22,AFF_1:30; then LIN b,b',a' or c in
A' by A13,AFF_1:26,33;
then a' in P by A2,A4,A14,AFF_1:39,def 2;
hence contradiction by A3,A4,AFF_1:59; end;
then a,c // a',y by A1,A2,A3,A4,A5,A25,A26,A27,Def6;
then a',y // a',c' by A5,A7,AFF_1:14; then LIN a',y,c' by AFF_1:def 1;
then LIN a',c',y by AFF_1:15; then y in N by AFF_1:def 2;
then N=C or y=c' by A2,A4,A8,A25,AFF_1:30; then a' in C or
LIN b',c',x by A25,AFF_1:15,26; then x in T by A3,A4,AFF_1:59,def 2;
then q in M or
c' in D by A8,A22,AFF_1:30; then a,c // p,q or LIN c,c',b
by A8,A17,A19,AFF_1:33,53;
then a,c // p,q or b in C by A2,A4,A11,AFF_1:39;
hence thesis by A3,A4,A6,AFF_1:59; end;
now assume not T // M; then consider x such that
A29: x in T & x in M by A8,A18,AFF_1:72;
not b,x // C proof assume b,x // C; then b,x // C &
C // P by A4,AFF_1:58; then b,x // P by AFF_1:57;
then x in P by A2,A4,AFF_1:37; then b' in M or
c' in P by A2,A4,A8,A29,AFF_1:30;
then b'=p or M=P' by A3,A4,A6,A13,A17,A18,AFF_1:30,59;
then LIN b,b',a or N // P' by A5,A17,AFF_1:15;
then a in P or N=P' by A2,A4,A8,A13,A14,AFF_1:39,59;
hence contradiction by A3,A4,A8,AFF_1:59,def 2; end;
then consider y such that
A30: y in C & LIN b,x,y by A2,AFF_1:73;
A31: LIN b,y,x & LIN b',c',x & a',c' // p,x
by A8,A17,A29,A30,AFF_1:15,33,53;
A32: not LIN b,a,y proof assume LIN b,a,y;
then LIN b,y,a & LIN b,y,b by AFF_1:15,16; then b=y or
LIN a,b,x by A31,AFF_1:17; then x in A' by A3,A4,A6,A30,AFF_1:59,def 2;
then A33: x=p or A'=M by A13,A17,A18,A29,AFF_1:30;
now assume x=p; then p=b' or T=P'
by A8,A13,A29,AFF_1:30; then LIN
b,b',a or c' in P' by A13,AFF_1:26,33;
then a in P by A2,A4,A14,AFF_1:39,def 2;
hence contradiction by A3,A4,AFF_1:59; end; then K=A' by A8,A13,A19,A33,
AFF_1:59;hence contradiction by A4,A8,AFF_1:def 2; end;
p<>x proof assume p=x; then p=b' or T=P'
by A8,A13,A29,AFF_1:30; then LIN
b,b',a or c' in P' by A13,AFF_1:26,33;
then a in P by A2,A4,A14,AFF_1:39,def 2;
hence contradiction by A3,A4,AFF_1:59; end;
then a',c' // a,y by A1,A2,A3,A4,A5,A30,A31,A32,Def6;
then a,c // a,y by A5,A7,AFF_1:14; then LIN a,c,y by AFF_1:def 1;
then y in K by AFF_1:def 2; then K=C or y=c by A2,A4,A8,A30,AFF_1:30;
then a in C or LIN b,c,x by A30,AFF_1:15,26;
then x in D by A3,A4,AFF_1:59,def 2; then q in M or c' in D by A8,A29,AFF_1:
30;
then a,c // p,q or LIN c,c',b by A8,A17,A19,AFF_1:33,53;
then a,c // p,q or b in C by A2,A4,A11,AFF_1:39;
hence thesis by A3,A4,A6,AFF_1:59; end;
hence thesis by A20,A21;
end;
theorem
AP satisfies_DES2_1 iff AP satisfies_DES2_3 proof
A1: AP satisfies_DES2_1 implies AP satisfies_DES2_3
proof assume A2: AP satisfies_DES2_1;
thus AP satisfies_DES2_3 proof let A,P,C,a,a',b,b',c,c',p,q;
assume A3: A is_line & P is_line & C is_line &
A<>P & A<>C & P<>C & a in A & a' in A & b in P &
b' in P & c in C & c' in C & A // P & not LIN b,a,c &
not LIN b',a',c' & p<>q & c <>c' & LIN b,a,p & LIN b',a',p &
LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q;
now A4: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A3,AFF_1:16;
set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
A5: A' is_line & P' is_line & C' is_line & a in A' & c in A'
& p in P' & q in P' & a' in C' & c' in C' by A3,A4,AFF_1:38;
A6: q<>c proof assume A7: q=c; then c,p // c,a by A3,AFF_1:13;
then LIN c,p,a by AFF_1:def 1; then LIN p,a,c & LIN p,a,b & LIN p,a,a
by A3,AFF_1:15,16; then a=p by A3,AFF_1:17;
then LIN a,a',b' by A3,AFF_1:15; then b' in A or a=a' by A3,AFF_1:39;
then a',c' // a',c by A3,AFF_1:13,59;
then LIN a',c',c by AFF_1:def 1; then LIN c,c',a' by AFF_1:15;
then A8: a' in C by A3,AFF_1:39; LIN c,c',b' by A3,A7,AFF_1:15;
then b' in C by A3,AFF_1:39;
hence contradiction by A3,A8,AFF_1:33; end;
A9: a<>p proof assume a=p;
then LIN a,c,q by A3,AFF_1:def 1;
then LIN c,q,a & LIN c,q,b & LIN c,q,c by A3,AFF_1:15,16;
hence contradiction by A3,A6,AFF_1:17; end;
A10: a<>a' proof assume A11: a=a'; then LIN p,a,b & LIN p,a,b' &
LIN p,a,a by A3,AFF_1:15,16; then LIN b,b',a by A9,AFF_1:17;
then b=b' or a in P by A3,AFF_1:39;
then LIN q,b,c & LIN q,b,c' & LIN q,b,b by A3,AFF_1:15,16,59
; then A12: q=b or
LIN c,c',b by AFF_1:17;
LIN a,c,c' by A3,A11,AFF_1:def 1; then LIN c,c',a
by AFF_1:15; then A13: a in C by A3,AFF_1:39;
then not b in C by A3,AFF_1:33;
then LIN p,q,a by A3,A12,AFF_1:15,39; then p,q // p,a
by AFF_1:def 1; then a,c // p,a by A3,AFF_1:14;
then a,c // a,p by AFF_1:13; then LIN a,c,p by AFF_1:def 1;
then p in C & LIN p,a,b by A3,A4,A13,AFF_1:15,39;
then b in C by A3,A9,A13,AFF_1:39;
hence contradiction by A3,A13,AFF_1:33; end;
A14: b<>b' proof assume A15: b=b'; then LIN p,b,a & LIN p,b,a' &
LIN p,b,b by A3,AFF_1:15,16; then p=b or LIN a,a',b by AFF_1:17;
then A16: p=b or b in A by A3,A10,AFF_1:39;
LIN q,b,c & LIN q,b,c' & LIN q,b,b by A3,A15,AFF_1:15,16;
then b=q or LIN c,c',b by AFF_1:17; then A17: b in C by A3,A16,AFF_1:39,
59;
then q in C & p in C & p,q // c,a by A3,A16,AFF_1:13,39,59;
then a in C by A3,AFF_1:62; hence contradiction by A3,A17,AFF_1:33; end
;
A18: A'<>P' proof assume A'=P'; then LIN p,a,c & LIN p,a,b &
LIN p,a,a by A3,A5,AFF_1:15,33;
hence contradiction by A3,A9,AFF_1:17; end;
A19: A'<>C' proof assume A'=C'; then LIN a,a',c & LIN a,a',c'
by A5,AFF_1:33; then c in A & c' in A by A3,A10,AFF_1:39;
hence contradiction by A3,AFF_1:30; end;
A20: P'<>C' proof assume P'=C'; then LIN p,a',c' & LIN p,a',b' &
LIN p,a',a' by A3,A5,AFF_1:15,33;
then p=a' by A3,AFF_1:17; then LIN a,a',b by A3,AFF_1:15;
then b in A by A3,A10,AFF_1:39;
hence contradiction by A3,AFF_1:59; end;
A21: a',c' // p,q & a',c' // a,c by A3,A4,AFF_1:13,14;
then A22: C' // P' & C' // A' & A' // P' by A3,A4,A5,AFF_1:52;
A23: a',a // b',b by A3,A10,A14,AFF_1:52;
A24: LIN p,a,b & LIN p,a',b' & LIN q,c,b & LIN q,c',b' by A3,AFF_1:15;
A25: not LIN p,a',a proof assume LIN p,a',a; then LIN p,a,a' &
LIN p,a,a by AFF_1:15,16; then LIN a,a',b by A9,A24,AFF_1:17;
then b in A by A3,A10,AFF_1:39;
hence contradiction by A3,AFF_1:59; end;
not LIN q,c',c proof assume A26: LIN q,c',c; then LIN q,c,c' &
LIN q,c,c by AFF_1:15,16; then LIN c,c',b by A6,A24,AFF_1:17;
then A27: b in C by A3,AFF_1:39;
LIN q,c',c' by AFF_1:16; then A28: LIN
c,c',b' or q=c' by A24,A26,AFF_1:17;
now assume q=c'; then c',a' // c',p by A21,AFF_1:13;
then LIN c',a',p by AFF_1:def 1; then p in C' by A4,A5,AFF_1:39;
then p=a' or b' in C' by A5,A24,AFF_1:39; then LIN a,a',b
by A3,A5,AFF_1:15,33; then b in A by A3,A10,AFF_1:39;
hence contradiction by A3,AFF_1:59; end;
then b' in C by A3,A28,AFF_1:39;
hence contradiction by A3,A14,A27,AFF_1:30; end;
then a',a // c',c by A2,A5,A14,A18,A19,A20,A22,A23,A24,A25,Def6;
hence A // C by A3,A10,AFF_1:52; end;
hence thesis; end;
end;
AP satisfies_DES2_3 implies AP satisfies_DES2_1
proof assume A29: AP satisfies_DES2_3;
thus AP satisfies_DES2_1 proof let A,P,C,a,a',b,b',c,c',p,q;
assume A30: A is_line & P is_line & C is_line &
A<>P & A<>C & P<>C & a in A & a' in A & b in P & b' in P &
c in C & c' in C & A // P & A // C & not LIN b,a,c &
not LIN b',a',c' & p<>q & LIN b,a,p & LIN b',a',p & LIN b,c,q &
LIN b',c',q & a,c // p,q;
assume A31: not thesis;
A32: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A30,AFF_1:16;
set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
A33: A' is_line & P' is_line & C' is_line & a in A' & c in A' &
p in P' & q in P' & a' in C' & c' in C' by A30,A32,AFF_1:38;
A34: C // A & C // P by A30,AFF_1:58;
then A35: c,c' // a,a' & c,c' // b,b' by A30,AFF_1:53;
A36: A' // P' by A30,A32,A33,AFF_1:52;
A37: q<>c proof assume A38: q=c; then c,p // c,a by A30,AFF_1:13;
then LIN c,p,a by AFF_1:def 1;
then LIN p,a,c & LIN p,a,b & LIN p,a,a by A30,AFF_1:15,16;
then a=p by A30,AFF_1:17; then LIN a,a',b' by A30,AFF_1:15;
then A39: b' in A or a=a' by A30,AFF_1:39;
LIN c,c',b' by A30,A38,AFF_1:15; then c =c' or b' in C by A30,AFF_1:39;
hence contradiction by A30,A31,A34,A39,AFF_1:11,59; end;
A40: a<>p proof assume a=p;
then LIN a,c,q by A30,AFF_1:def 1;
then LIN c,q,a & LIN c,q,b & LIN c,q,c by A30,AFF_1:15,16;
hence contradiction by A30,A37,AFF_1:17; end;
A41: a<>a' proof assume A42: a=a'; then LIN p,a,b & LIN p,a,b' &
LIN p,a,a by A30,AFF_1:15,16; then LIN b,b',a by A40,AFF_1:17;
then a in P or b=b' by A30,AFF_1:39;
then LIN b,q,c & LIN b,q,c' & LIN b,q,b by A30,AFF_1:15,16,59;
then b=q or LIN c,c',b by AFF_1:17;
then b=q or c =c' or b in
C by A30,AFF_1:39; then LIN p,q,a by A30,A31,A34,A42,AFF_1:11,15,59;
then p,q // p,a by AFF_1:def 1; then a,c // p,a by A30,AFF_1:14;
then a,c // a,p by AFF_1:13; then LIN a,c,p by AFF_1:def 1;
then LIN p,a,c & LIN p,a,b & LIN p,a,a by A30,AFF_1:15,16;
hence contradiction by A30,A40,AFF_1:17; end;
A43: A'<>P' proof assume A'=P'; then LIN p,a,c & LIN p,a,b &
LIN p,a,a by A30,A33,AFF_1:15,33;
hence contradiction by A30,A40,AFF_1:17; end;
A44: A'<>C' by A31,A33,AFF_1:65;
A45: b<>b' proof assume b=b'; then LIN b,p,a & LIN b,p,a' &
LIN b,p,b by A30,AFF_1:15,16; then b=p or LIN a,a',b by AFF_1:17;
then A46: b=p or b in A by A30,A41,AFF_1:39;
then LIN p,q,c by A30,AFF_1:15,59;
then p,q // p,c by AFF_1:def 1;
then a,c // p,c by A30,AFF_1:14; then c,a // c,p by AFF_1:13;
then LIN c,a,p by AFF_1:def 1; hence contradiction by A30,A46,AFF_1:15,59
; end;
A47: not LIN q,c,c' proof assume A48: LIN q,c,c'; LIN q,c,b &
LIN q,c,c by A30,AFF_1:15,16; then LIN c,c',b by A37,A48,AFF_1:17;
then c =c' or b in C by A30,AFF_1:39;
then LIN q,c,b & LIN q,c,b' & LIN
q,c,c by A30,A34,AFF_1:15,16,59
;
then LIN b,b',c by A37,AFF_1:17; then c in P by A30,A45,AFF_1:39;
hence contradiction by A30,A34,AFF_1:59; end;
A49: not LIN p,a,a' proof assume LIN p,a,a'; then LIN p,a,a' &
LIN p,a,b & LIN p,a,a by A30,AFF_1:15,16;
then LIN a,a',b by A40,AFF_1:17; then b in A by A30,A41,AFF_1:39;
hence contradiction by A30,AFF_1:59; end;
LIN q,c,b & LIN q,c',b' & LIN p,a,b & LIN p,a',b' by A30,AFF_1:15;
then A' // C' by A29,A32,A33,A35,A36,A43,A44,A45,A47,A49,Def8;
hence contradiction by A31,A33,AFF_1:53;
end;
end;
hence thesis by A1; end;
theorem
AP satisfies_DES2 iff AP satisfies_DES2_2 proof
A1: AP satisfies_DES2 implies AP satisfies_DES2_2
proof assume A2: AP satisfies_DES2;
thus AP satisfies_DES2_2 proof let A,P,C,a,a',b,b',c,c',p,q;
assume A3: A is_line & P is_line & C is_line & A<>P &
A<>C & P<>C & a in A & a' in A & b in P & b' in P & c in C &
c' in C & A // C & not LIN b,a,c & not LIN b',a',c' & p<>q &
a<>a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c' & a,c // p,q;
then A4: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by AFF_1:16;
A5: a<>p proof assume A6: a=p; then LIN a,a',b' by A3,AFF_1:15;
then A7: b' in A by A3,AFF_1:39;
LIN a,c,q by A3,A6,AFF_1:def 1;
then LIN c,q,a & LIN c,q,b & LIN c,q,c by A3,AFF_1:15,16;
then q=c by A3,AFF_1:17; then LIN c,c',b' by A3,AFF_1:15; then c =c' or
b' in C by A3,AFF_1:39; then c,a // c,a' by A3,A7,AFF_1:13,59;
then LIN c,a,a' by AFF_1:def 1; then LIN a,a',c by AFF_1:15; then c in A
by A3,AFF_1:39; hence contradiction by A3,AFF_1:59; end;
A8: q<>c proof assume q=c; then c,p // c,a by A3,AFF_1:13;
then LIN c,p,a by AFF_1:def 1; then LIN p,a,c & LIN p,a,b & LIN p,a,a by A3,
AFF_1:15,16; hence contradiction by A3,A5,AFF_1:17; end;
A9: c <>c' proof assume c =c'; then c,a // c,a' by A3,AFF_1:13;
then LIN c,a,a' by AFF_1:def 1; then LIN a,a',c by AFF_1:15; then c in A
by A3,AFF_1:39; hence contradiction by A3,AFF_1:59; end;
A10: a'<>p proof assume A11: a'=p; then LIN a,a',b by A3,AFF_1:15;
then A12: b in A by A3,AFF_1:39; a',c' // p,q by A3,A4,AFF_1:14;
then LIN a',c',q by A11,AFF_1:def 1; then LIN c',q,a' & LIN c',q,b' &
LIN c',q,c' by A3,AFF_1:15,16; then q=c' by A3,AFF_1:17;
then LIN c,c',b by A3,AFF_1:15; then b in C by A3,A9,AFF_1:39;
hence contradiction by A3,A12,AFF_1:59; end;
A13: c'<>q proof assume c'=q;
then a',c' // p,c' by A3,A4,AFF_1:14; then c',a' // c',p by AFF_1:13;
then LIN c',a',p by AFF_1:def 1; then LIN p,a',c' & LIN p,a',b' & LIN p,a'
,a' by A3,AFF_1:15,16; hence contradiction by A3,A10,AFF_1:17; end;
A14: b<>b' proof assume b=b'; then LIN b,p,a & LIN b,p,a' &
LIN b,p,b & LIN b,q,c & LIN b,q,c' & LIN b,q,b by A3,AFF_1:15,16;
then (b=p or LIN a,a',b) & (b=q or LIN c,c',b) by AFF_1:17;
then A15: (b=p or b in A) & (b=q or b in C) by A3,A9,AFF_1:39;
A16: now assume A17: b=p & b in C; then LIN p,q,c & p in C by A3,AFF_1:15;
then p,q // p,c by AFF_1:def 1;
then a,c // p,c by A3,AFF_1:14; then c,a // c,p by AFF_1:13;
then LIN c,a,p by AFF_1:def 1;
hence contradiction by A3,A17,AFF_1:15; end;
then q in A & LIN q,p,a by A3,A15,AFF_1:15,59;
then q in A & q,p // q,a by AFF_1:def 1; then q in A & p,q // q,a
by AFF_1:13; then q in A & a,c // q,a by A3,AFF_1:14; then q in A &
a,c // a,q by AFF_1:13; then q in A & LIN a,c,q by AFF_1:def 1;
then q in A & LIN a,q,c by AFF_1:15; then c in A or a=q by A3,AFF_1:39;
hence contradiction by A3,A15,A16,AFF_1:16,59; end;
set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
A18: A' is_line & P' is_line & C' is_line & a in A' & c in A' &
p in P' & q in P' & a' in C' & c' in C' by A3,A4,AFF_1:38;
a',c' // a,c & a',c' // p,q by A3,A4,AFF_1:13,14;
then A19: C' // A' & C' // P' by A3,A4,A18,AFF_1:52;
A20: C'<>A' proof assume C'=A'; then LIN a,a',c by A18,AFF_1:33;
then c in A by A3,AFF_1:39;
hence contradiction by A3,AFF_1:59; end;
A21: C'<>P' proof assume C'=P'; then LIN p,a',c' & LIN p,a',b' &
LIN p,a',a' by A3,A18,AFF_1:15,33;
hence contradiction by A3,A10,AFF_1:17; end;
A22: P'<>A' proof assume P'=A'; then LIN p,a,c & LIN p,a,b &
LIN p,a,a by A3,A18,AFF_1:15,33;
hence contradiction by A3,A5,AFF_1:17; end;
A23: LIN p,a',b' & LIN p,a,b & LIN q,c',b' & LIN q,c,b by A3,AFF_1:15;
A24: not LIN p,a',a proof assume LIN p,a',a; then LIN p,a',a &
LIN p,a',a' & LIN p,a,a' & LIN p,a,a by AFF_1:15,16;
then LIN a,a',b' & LIN a,a',b by A5,A10,A23,AFF_1:17;
then b in A & b' in A by A3,AFF_1:39;
hence contradiction by A3,A14,AFF_1:30; end;
A25: not LIN q,c',c proof assume LIN q,c',c; then LIN q,c',c &
LIN q,c',c' & LIN q,c,c' & LIN q,c,c by AFF_1:15,16;
then LIN c,c',b & LIN c,c',b' by A8,A13,A23,AFF_1:17;
then b in C & b' in C by A3,A9,AFF_1:39;
hence contradiction by A3,A14,AFF_1:30; end;
a',a // c',c by A3,AFF_1:53;
then a',a // b',b by A2,A4,A14,A18,A19,A20,A21,A22,A23,A24,A25,Def5;
hence A // P by A3,A14,AFF_1:52; end;
end;
AP satisfies_DES2_2 implies AP satisfies_DES2
proof assume A26: AP satisfies_DES2_2;
thus AP satisfies_DES2 proof let A,P,C,a,a',b,b',c,c',p,q;
assume A27: A is_line & P is_line & C is_line & A<>P & A<>C &
P<>C & a in A & a' in A & b in P & b' in P & c in C &
c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' &
p<>q & a<>a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
a,c // a',c';
then A28: C // P & C // A by AFF_1:58;
A29: a<>b & a<>c & b<>c & a'<>b' & a'<>c' & b'<>c' by A27,AFF_1:16;
A30: c <>c' proof assume c =c'; then c,a // c,a' by A27,AFF_1:13;
then LIN c,a,a' by AFF_1:def 1; then LIN a,a',c by AFF_1:15; then c in A
by A27,AFF_1:39; hence contradiction by A27,AFF_1:59; end;
A31: a<>p proof assume a=p; then LIN a,a',b' by A27,AFF_1:15; then b' in A
by A27,AFF_1:39; hence contradiction by A27,AFF_1:59; end;
A32: q<>c proof assume q=c; then LIN c,c',b' by A27,AFF_1:15; then b' in C
by A27,A30,AFF_1:39; hence contradiction by A27,A28,AFF_1:59; end;
A33: b<>b' proof assume b=b'; then LIN b,p,a & LIN b,p,a' &
LIN b,p,b & LIN b,q,c & LIN b,q,c' & LIN
b,q,b by A27,AFF_1:15,16;
then (b=p or LIN a,a',b) & (b=q or LIN c,c',b) by AFF_1:17;
then (b=p or b in A) & (b=q or b in C) by A27,A30,AFF_1:39;
hence contradiction by A27,A28,AFF_1:59; end;
set A'=Line(a,c), P'=Line(p,q), C'=Line(a',c');
A34: A' is_line & P' is_line & C' is_line & a in A' & c in A' &
p in P' & q in P' & a' in C' & c' in C' by A27,A29,AFF_1:38;
A35: c,c' // a,a' & c,c' // b,b' by A27,A28,AFF_1:53;
A36: LIN q,c,b & LIN q,c',b' & LIN p,a,b & LIN p,a',b' by A27,AFF_1:15;
A37: A' // C' by A27,A29,A34,AFF_1:52;
A38: A'<>P' proof assume A'=P'; then LIN c,q,a & LIN c,q,b &
LIN c,q,c by A27,A34,AFF_1:15,33;
hence contradiction by A27,A32,AFF_1:17; end;
A39: A'<>C' proof assume A'=C'; then LIN a,a',c by A34,AFF_1:33;
then c in A by A27,AFF_1:39;
hence contradiction by A27,AFF_1:59; end;
A40: not LIN q,c,c' proof assume LIN q,c,c'; then LIN q,c,c' &
LIN q,c,c by AFF_1:16; then LIN c,c',b by A32,A36,AFF_1:17; then b in C
by A27,A30,AFF_1:39; hence contradiction by A27,A28,AFF_1:59; end;
not LIN p,a,a' proof assume LIN p,a,a'; then LIN p,a,a' &
LIN p,a,a by AFF_1:16; then LIN a,a',b by A31,A36,AFF_1:17; then b in A
by A27,AFF_1:39; hence contradiction by A27,AFF_1:59; end;
then A' // P' by A26,A29,A33,A34,A35,A36,A37,A38,A39,A40,Def7;
hence thesis by A34,AFF_1:53; end;
end;
hence thesis by A1;
end;
theorem
AP satisfies_DES1_3 implies AP satisfies_DES2_1
proof assume A1: AP satisfies_DES1_3;
let A,P,C,a,a',b,b',c,c',p,q such that
A2: A is_line and
A3: P is_line and
A4: C is_line and
A5: A<>P and
A6: A<>C and
A7: P<>C and
A8: a in A and
A9: a' in A and
A10: b in P and
A11: b' in P and
A12: c in C and
A13: c' in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b',a',c' and
A18: p<>q and
A19: LIN b,a,p and
A20: LIN b',a',p and
A21: LIN b,c,q and
A22: LIN b',c',q and
A23: a,c // p,q;
assume A24: not thesis;
A25: a<>b & b<>c & a<>c & a'<>b' & a'<>c' & b'<>c' by A16,A17,AFF_1:16;
A26: P // C by A14,A15,AFF_1:58;
A27: c <>q proof assume A28: c =q; then LIN c,c',b' by A22,AFF_1:15;
then A29: c =c' or b' in C by A4,A12,A13,AFF_1:39;
c,a // c,p by A23,A28,AFF_1:13; then LIN c,a,p by AFF_1:def 1;
then LIN p,a,c & LIN p,a,b & LIN p,a,a by A19,AFF_1:15,16;
then p=a by A16,AFF_1:17; then LIN a,a',b' by A20,AFF_1:15;
then a=a' or b' in A by A2,A8,A9,AFF_1:39;
hence contradiction by A5,A7,A11,A14,A24,A26,A29,AFF_1:11,59; end;
A30: c <>c' proof assume A31: c =c'; then LIN q,c,b & LIN q,c,b' &
LIN q,c,c by A21,A22,AFF_1:15,16; then LIN b,b',c by A27,AFF_1:17;
then b=b' or c in P by A3,A10,A11,AFF_1:39;
then LIN p,b,a' & LIN p,b,a & LIN p,b,b
by A7,A12,A19,A20,A26,AFF_1:15,16,59;
then A32: p=b or LIN a,a',b by AFF_1:17;
now assume A33: p=b; then a,c // b,q & LIN b,q,c by A21,A23,AFF_1:15;
then a,c // b,q & b,q // b,c by AFF_1:def 1; then a,c // b,c or
b=q by AFF_1:14; then c,a // c,b by A18,A33,AFF_1:13; then LIN c,a,b
by AFF_1:def 1; hence contradiction by A16,AFF_1:15; end; then a=a' or
b in A by A2,A8,A9,A32,AFF_1:39;
hence contradiction by A5,A10,A14,A24,A31,AFF_1:11,59; end;
set K=Line(p,q), M=Line(a,c), N=Line(a',c');
A34: K is_line & M is_line & N is_line & p in K &
q in K & a in M & c in M & a' in N & c' in N
by A18,A25,AFF_1:38; then A35: M // K by A18,A23,A25,AFF_1:52;
not M // N by A24,A34,AFF_1:53; then consider
x such that A36: x in M & x in N by A34,AFF_1:72;
C // P & C // A by A14,A15,AFF_1:58;
then A37: c,c' // b,b' & c,c' // a,a' by A8,A9,A10,A11,A12,A13,AFF_1:53;
A38: LIN q,c,b & LIN q,c',b' & LIN p,a,b & LIN p,a',b'
by A19,A20,A21,A22,AFF_1:15;
A39: b<>b' proof assume b=b'; then LIN q,b,c & LIN q,b,c' &
LIN q,b,b by A21,A22,AFF_1:15,16;
then q=b or LIN c,c',b by AFF_1:17;
then A40: q=b or b in C by A4,A12,A13,A30,AFF_1:39;
then a,c // p,b &
b,a // b,p by A7,A10,A19,A23,A26,AFF_1:59,def 1;
then a,c // p,b & a,b // p,b
by AFF_1:13; then a,c // a,b or p=b by AFF_1:14; then LIN a,c,b by A7,A10,A18
,A26,A40,AFF_1:59,def 1;
hence contradiction by A16,AFF_1:15;
end;
A41: p<>a proof assume p=a; then LIN a,c,q
by A23,AFF_1:def 1; then LIN c,q,a & LIN c,q,b & LIN
c,q,c by A21,AFF_1:15,16;
hence contradiction by A16,A27,AFF_1:17; end;
A42: now assume M=K; then LIN q,c,a & LIN q,c,b & LIN q,c,c by A21,A34,AFF_1:
15,33;
hence contradiction by A16,A27,AFF_1:17; end;
A43: M<>N by A24,A34,AFF_1:65;
A44: now assume x=c; then N=C by A4,A12,A13,A30,A34,A36,AFF_1:30;
hence contradiction by A6,A9,A15,A34,AFF_1:59; end;
A45: now assume x=c'; then M=C by A4,A12,A13,A30,A34,A36,AFF_1:30;
hence contradiction by A6,A8,A15,A34,AFF_1:59; end;
A46: not LIN q,c,c' proof assume LIN q,c,c'; then LIN q,c,c' & LIN q,c,b &
LIN q,c,c by A21,AFF_1:15,16; then LIN c,c',b by A27,AFF_1:17;
then b in C by A4,A12,A13,A30,AFF_1:39;
hence contradiction by A7,A10,A26,AFF_1:59; end;
not LIN p,a,a' proof assume LIN p,a,a'; then LIN p,a,a' &
LIN p,a,b & LIN p,a,a by A19,AFF_1:15,16;
then LIN a,a',b by A41,AFF_1:17; then a=a' or b in A by A2,A8,A9,AFF_1:39;
then LIN p,a,b & LIN p,a,b' & LIN p,a,a
by A5,A10,A14,A19,A20,AFF_1:15,16,59;
then LIN b,b',a
by A41,AFF_1:17; then a in P by A3,A10,A11,A39,AFF_1:39;
hence contradiction by A5,A8,A14,AFF_1:59; end;
then x in K by A1,A18,A25,A34,A36,A37,A38,A39,A43,A44,A45,A46,Def4;
hence contradiction by A35,A36,A42,AFF_1:59;
end;