:: Affine Localizations of Desargues Axiom
:: by Eugeniusz Kusak, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 26, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies DIRAF, SUBSET_1, AFF_1, ANALOAF, INCSP_1, AFF_2, AFF_3;
notations STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2;
constructors AFF_1, AFF_2;
registrations STRUCT_0;
definitions AFF_2;
expansions AFF_2;
theorems AFF_1, AFF_2;
begin
reserve AP for AffinPlane;
reserve a,a9,b,b9,c,c9,d,x,y,o,p,q for Element of AP;
reserve A,C,D9,M,N,P for Subset of AP;
definition
let AP;
attr AP is satisfying_DES1 means
for A,P,C,o,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in A
& a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o
<>a & o<>b & o<>c & p<>q & not LIN b,a,c & not LIN b9,a9,c9 & a<>a9 & LIN b,a,p
& LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q;
end;
definition
let AP;
attr AP is satisfying_DES1_1 means
for A,P,C,o,a,a9,b,b9,c,c9,p,q st
A is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in
A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C &
o<>a & o<>b & o<>c & p<>q & c <>q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,
p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9;
end;
definition
let AP;
attr AP is satisfying_DES1_2 means
for A,P,C,o,a,a9,b,b9,c,c9,p,q st
A is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in
A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o<>a & o
<>b & o<>c & p<>q & not LIN b,a,c & not LIN b9,a9,c9 & c <>c9 & LIN b,a,p & LIN
b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C;
end;
definition
let AP;
attr AP is satisfying_DES1_3 means
for A,P,C,o,a,a9,b,b9,c,c9,p,q st
A is being_line & P is being_line & C is being_line & P<>A & P<>C & A<>C & o in
A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o<>a & o
<>b & o<>c & p<>q & not LIN b,a,c & not LIN b9,a9,c9 & b<>b9 & a<>a9 & LIN b,a,
p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o
in P;
end;
definition
let AP;
attr AP is satisfying_DES2 means
for A,P,C,a,a9,b,b9,c,c9,p,q st A is
being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A &
a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c
& not LIN b9,a9,c9 & p<>q & a<>a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN
b9,c9,q & a,c // a9,c9 holds a,c // p,q;
end;
definition
let AP;
attr AP is satisfying_DES2_1 means
for A,P,C,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A
& a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a
,c & not LIN b9,a9,c9 & p<>q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,
q & a,c // p,q holds a,c // a9,c9;
end;
definition
let AP;
attr AP is satisfying_DES2_2 means
for A,P,C,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A
& a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not
LIN b9,a9,c9 & p<>q & a<>a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q
& a,c // a9,c9 & a,c // p,q holds A // P;
end;
definition
let AP;
attr AP is satisfying_DES2_3 means
for A,P,C,a,a9,b,b9,c,c9,p,q st A
is being_line & P is being_line & C is being_line & A<>P & A<>C & P<>C & a in A
& a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not
LIN b9,a9,c9 & p<>q & c <>c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,
q & a,c // a9,c9 & a,c // p,q holds A // C;
end;
theorem
AP is satisfying_DES1 implies AP is satisfying_DES1_1
proof
assume
A1: AP is satisfying_DES1;
let A,P,C,o,a,a9,b,b9,c,c9,p,q;
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P<>A and
A6: P<>C and
A7: A<>C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: o in P and
A12: b in P & b9 in P and
A13: o in C & c in C and
A14: c9 in C and
A15: o<>a and
A16: o<>b and
A17: o<>c and
A18: p<>q and
A19: c <>q and
A20: not LIN b,a,c and
A21: not LIN b9,a9,c9 and
A22: LIN b,a,p and
A23: LIN b9,a9,p and
A24: LIN b,c,q and
A25: LIN b9,c9,q and
A26: a,c // p,q;
A27: LIN o,a,a9 & LIN b9,p,a9 by A2,A8,A9,A10,A23,AFF_1:6,21;
set K=Line(b,a);
A28: a in K by AFF_1:15;
then
A29: K<>P by A2,A3,A5,A8,A9,A11,A15,AFF_1:18;
A30: not LIN o,a,c
proof
assume LIN o,a,c;
then c in A by A2,A8,A9,A15,AFF_1:25;
hence contradiction by A2,A4,A7,A8,A13,A17,AFF_1:18;
end;
A31: p in K by A22,AFF_1:def 2;
A32: LIN o,c,c9 & LIN b9,q,c9 by A4,A13,A14,A25,AFF_1:6,21;
A33: b<>c & a <> p by A19,A20,A24,A26,AFF_1:7,14;
A34: a9<>c9 & b<>a by A20,A21,AFF_1:7;
b<>a by A20,AFF_1:7;
then
A35: K is being_line by AFF_1:def 3;
set M=Line(b,c);
A36: c in M by AFF_1:15;
then
A37: M<>P by A3,A4,A6,A11,A13,A17,AFF_1:18;
b<>c by A20,AFF_1:7;
then
A38: M is being_line by AFF_1:def 3;
A39: b in M & q in M by A24,AFF_1:15,def 2;
q<>b
proof
assume
A40: q=b;
( not LIN b,c,a)& c,a // q,p by A20,A26,AFF_1:4,6;
hence contradiction by A18,A22,A40,AFF_1:55;
end;
then
A41: q<>b9 by A3,A12,A38,A39,A37,AFF_1:18;
A42: b in K by AFF_1:15;
p<>b by A18,A20,A24,A26,AFF_1:55;
then
A43: p<>b9 by A3,A12,A35,A42,A31,A29,AFF_1:18;
A44: not LIN b9,p,q
proof
set N=Line(p,q);
A45: N is being_line by A18,AFF_1:def 3;
assume LIN b9,p,q;
then LIN p,q,b9 by AFF_1:6;
then
A46: b9 in N by AFF_1:def 2;
q in N & LIN q,b9,c9 by A25,AFF_1:6,15;
then
A47: c9 in N by A41,A45,A46,AFF_1:25;
p in N & LIN p,b9,a9 by A23,AFF_1:6,15;
then a9 in N by A43,A45,A46,AFF_1:25;
hence contradiction by A21,A45,A46,A47,AFF_1:21;
end;
K<>M by A20,A35,A42,A28,A36,AFF_1:21;
hence
thesis by A1,A3,A11,A12,A16,A26,A35,A38,A42,A28,A36,A31,A39,A37,A29,A34,A30
,A44,A33,A27,A32;
end;
theorem
AP is satisfying_DES1_1 implies AP is satisfying_DES1
proof
assume
A1: AP is satisfying_DES1_1;
let A,P,C,o,a,a9,b,b9,c,c9,p,q;
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P<>A and
A6: P<>C and
A7: A<>C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: o in P and
A12: b in P and
A13: b9 in P and
A14: o in C and
A15: c in C and
A16: c9 in C and
A17: o<>a and
A18: o<>b and
A19: o<>c and
A20: p<>q and
A21: not LIN b,a,c and
A22: not LIN b9,a9,c9 and
A23: a<>a9 and
A24: LIN b,a,p and
A25: LIN b9,a9,p and
A26: LIN b,c,q and
A27: LIN b9,c9,q and
A28: a,c // a9,c9;
A29: a9<>b9 by A22,AFF_1:7;
set M=Line(b,c);
A30: c in M by AFF_1:15;
then
A31: M<>P by A3,A4,A6,A11,A14,A15,A19,AFF_1:18;
A32: M<>P by A3,A4,A6,A11,A14,A15,A19,A30,AFF_1:18;
A33: b in M by AFF_1:15;
set K=Line(b,a);
A34: a in K by AFF_1:15;
then
A35: K<>P by A2,A3,A5,A8,A9,A11,A17,AFF_1:18;
A36: p in K by A24,AFF_1:def 2;
A37: a9<>c9 & b<>a by A21,A22,AFF_1:7;
A38: b<>c by A21,AFF_1:7;
A39: q in M by A26,AFF_1:def 2;
A40: b9<>c9 by A22,AFF_1:7;
A41: b in K by AFF_1:15;
A42: not LIN o,a,c
proof
assume LIN o,a,c;
then c in A by A2,A8,A9,A17,AFF_1:25;
hence contradiction by A2,A4,A7,A8,A14,A15,A19,AFF_1:18;
end;
A43: c <>c9
proof
assume c =c9;
then
A44: c,a // c,a9 by A28,AFF_1:4;
LIN o,a,a9 & not LIN o,c,a by A2,A8,A9,A10,A42,AFF_1:6,21;
hence contradiction by A23,A44,AFF_1:14;
end;
b<>c by A21,AFF_1:7;
then
A45: M is being_line by AFF_1:def 3;
b<>a by A21,AFF_1:7;
then
A46: K is being_line by AFF_1:def 3;
A47: K<>P by A2,A3,A5,A8,A9,A11,A17,A34,AFF_1:18;
A48: now
set C9=Line(b9,c9);
set A9=Line(b9,a9);
A49: c9 in C9 by AFF_1:15;
A50: A9 is being_line & b9 in A9 by A29,AFF_1:15,def 3;
A51: a9 in A9 by AFF_1:15;
then
A52: A9<>C9 by A22,A50,A49,AFF_1:21;
A53: q in C9 by A27,AFF_1:def 2;
A54: p in A9 by A25,AFF_1:def 2;
A55: C9 is being_line & b9 in C9 by A40,AFF_1:15,def 3;
assume
A56: LIN b9,p,q;
then
A57: LIN b9,q,p by AFF_1:6;
A58: now
A59: C9<>M
proof
assume C9=M;
then LIN c,c9,b by A45,A33,A30,A49,AFF_1:21;
then b in C by A4,A15,A16,A43,AFF_1:25;
hence contradiction by A3,A4,A6,A11,A12,A14,A18,AFF_1:18;
end;
assume b9<>q;
then
A60: p in C9 by A57,A55,A53,AFF_1:25;
then LIN b,a,b9 by A24,A50,A54,A55,A52,AFF_1:18;
then b9 in K by AFF_1:def 2;
then
A61: b=b9 by A3,A12,A13,A46,A41,A47,AFF_1:18;
p=b9 by A50,A54,A55,A52,A60,AFF_1:18;
then p=q by A45,A33,A39,A55,A53,A61,A59,AFF_1:18;
hence thesis by AFF_1:3;
end;
now
A62: A9<>K
proof
assume A9=K;
then LIN a,a9,b by A46,A41,A34,A51,AFF_1:21;
then b in A by A2,A9,A10,A23,AFF_1:25;
hence contradiction by A2,A3,A5,A8,A11,A12,A18,AFF_1:18;
end;
assume b9<>p;
then
A63: q in A9 by A56,A50,A54,AFF_1:25;
then LIN b,c,b9 by A26,A50,A55,A53,A52,AFF_1:18;
then b9 in M by AFF_1:def 2;
then
A64: b=b9 by A3,A12,A13,A45,A33,A32,AFF_1:18;
q=b9 by A50,A55,A53,A52,A63,AFF_1:18;
then p=q by A46,A41,A36,A50,A54,A64,A62,AFF_1:18;
hence thesis by AFF_1:3;
end;
hence thesis by A20,A58;
end;
A65: K<>M by A21,A46,A41,A34,A30,AFF_1:21;
now
A66: LIN o,c,c9 & LIN b9,q,c9 by A4,A14,A15,A16,A27,AFF_1:6,21;
assume
A67: not LIN b9,p,q;
LIN o,a,a9 & LIN b9,p,a9 by A2,A8,A9,A10,A25,AFF_1:6,21;
hence
thesis by A1,A3,A11,A12,A13,A18,A28,A46,A45,A41,A34,A33,A30,A36,A39,A31,A35
,A37,A38,A65,A42,A43,A67,A66;
end;
hence thesis by A48;
end;
theorem
AP is Desarguesian implies AP is satisfying_DES1
proof
assume
A1: AP is Desarguesian;
let A,P,C,o,a,a9,b,b9,c,c9,p,q;
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P<>A and
A6: P<>C and
A7: A<>C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: o in P and
A12: b in P and
A13: b9 in P and
A14: o in C and
A15: c in C and
A16: c9 in C and
A17: o<>a and
A18: o<>b and
A19: o<>c and
p<>q and
A20: not LIN b,a,c and
A21: not LIN b9,a9,c9 and
A22: a<>a9 and
A23: LIN b,a,p and
A24: LIN b9,a9,p and
A25: LIN b,c,q and
A26: LIN b9,c9,q and
A27: a,c // a9,c9;
set D=Line(b,c);
b<>c by A20,AFF_1:7;
then D is being_line by AFF_1:def 3;
then consider D9 such that
A28: c9 in D9 and
A29: D // D9 by AFF_1:49;
A30: D9 is being_line by A29,AFF_1:36;
set M=Line(b9,c9);
A31: q in M by A26,AFF_1:def 2;
A32: b in D by AFF_1:15;
A33: c in D by AFF_1:15;
not D9 // P
proof
assume D9 // P;
then D // P by A29,AFF_1:44;
then c in P by A12,A32,A33,AFF_1:45;
hence contradiction by A3,A4,A6,A11,A14,A15,A19,AFF_1:18;
end;
then consider d such that
A34: d in D9 and
A35: d in P by A3,A30,AFF_1:58;
A36: q in D by A25,AFF_1:def 2;
then
A37: d,c9 // b,q by A32,A28,A29,A34,AFF_1:39;
A38: a<>b & b,a // b,p by A20,A23,AFF_1:7,def 1;
A39: c,a // c9,a9 by A27,AFF_1:4;
c,b // c9,d by A32,A33,A28,A29,A34,AFF_1:39;
then b,a // d,a9 by A1,A2,A3,A4,A6,A7,A8,A9,A10,A11,A12,A14,A15,A16,A17,A18
,A19,A35,A39;
then
A40: d,a9 // b,p by A38,AFF_1:5;
set K=Line(b9,a9);
A41: b9 in K & p in K by A24,AFF_1:15,def 2;
A42: a9<>b9 by A21,AFF_1:7;
then
A43: K is being_line by AFF_1:def 3;
A44: b9 in M by AFF_1:15;
A45: c9 in M by AFF_1:15;
A46: b9<>c9 by A21,AFF_1:7;
then
A47: M is being_line by AFF_1:def 3;
A48: not LIN o,a,c
proof
assume LIN o,a,c;
then c in A by A2,A8,A9,A17,AFF_1:25;
hence contradiction by A2,A4,A7,A8,A14,A15,A19,AFF_1:18;
end;
A49: c <>c9
proof
assume c =c9;
then
A50: c,a // c,a9 by A27,AFF_1:4;
LIN o,a,a9 & not LIN o,c,a by A2,A8,A9,A10,A48,AFF_1:6,21;
hence contradiction by A22,A50,AFF_1:14;
end;
A51: d<>b9
proof
assume d=b9;
then M=D9 by A46,A47,A44,A45,A28,A30,A34,AFF_1:18;
then D=M by A31,A36,A29,AFF_1:45;
then LIN c,c9,b by A47,A45,A32,A33,AFF_1:21;
then b in C by A4,A15,A16,A49,AFF_1:25;
hence contradiction by A3,A4,A6,A11,A12,A14,A18,AFF_1:18;
end;
A52: a9<>c9 by A21,AFF_1:7;
A53: o<>a9 by A4,A14,A15,A16,A27,A52,A48,AFF_1:21,55;
o<>c9
proof
A54: not LIN o,c,a by A48,AFF_1:6;
assume
A55: o=c9;
LIN o,a,a9 & c,a // c9,a9 by A2,A8,A9,A10,A27,AFF_1:4,21;
hence contradiction by A53,A55,A54,AFF_1:55;
end;
then
A56: M<>P by A3,A4,A6,A11,A14,A16,A45,AFF_1:18;
A57: a9 in K by AFF_1:15;
then K<>P by A2,A3,A5,A8,A10,A11,A53,AFF_1:18;
then a9,c9 // p,q by A1,A3,A12,A13,A42,A46,A43,A47,A57,A41,A44,A45,A31,A56
,A35,A51,A40,A37;
hence thesis by A27,A52,AFF_1:5;
end;
theorem
AP is Desarguesian implies AP is satisfying_DES1_2
proof
assume
A1: AP is Desarguesian;
then
A2: AP is satisfying_DES_1 by AFF_2:2;
let A,P,C,o,a,a9,b,b9,c,c9,p,q;
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: P<>A and
A7: P<>C and
A<>C and
A8: o in A and
A9: a in A & a9 in A and
A10: o in P and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: o<>a and
A16: o<>b and
o<>c and
A17: p<>q and
A18: not LIN b,a,c and
A19: not LIN b9,a9,c9 and
A20: c <>c9 and
A21: LIN b,a,p and
A22: LIN b9,a9,p and
A23: LIN b,c,q and
A24: LIN b9,c9,q and
A25: a,c // a9,c9 and
A26: a,c // p,q;
A27: b<>p by A17,A18,A23,A26,AFF_1:55;
set K=Line(b9,a9);
A28: p in K by A22,AFF_1:def 2;
a9<>b9 by A19,AFF_1:7;
then
A29: K is being_line by AFF_1:def 3;
A30: b<>q
proof
assume
A31: b=q;
( not LIN b,c,a)& c,a // q,p by A18,A26,AFF_1:4,6;
hence contradiction by A17,A21,A31,AFF_1:55;
end;
set M=Line(b9,c9);
A32: q in M by A24,AFF_1:def 2;
A33: c9 in M by AFF_1:15;
A34: a<>c by A18,AFF_1:7;
A35: b9<>p
proof
assume
A36: b9=p;
a9,c9 // p,q by A25,A26,A34,AFF_1:5;
hence contradiction by A17,A19,A24,A36,AFF_1:55;
end;
A37: b9<>q
proof
a9,c9 // p,q by A25,A26,A34,AFF_1:5;
then
A38: c9,a9 // q,p by AFF_1:4;
assume
A39: b9=q;
not LIN b9,c9,a9 by A19,AFF_1:6;
hence contradiction by A17,A22,A39,A38,AFF_1:55;
end;
A40: b<>c by A18,AFF_1:7;
A41: a<>b by A18,AFF_1:7;
A42: b9<>a9 & b9<>c9 by A19,AFF_1:7;
A43: a9 in K by AFF_1:15;
A44: b9 in M by AFF_1:15;
A45: b9<>c9 by A19,AFF_1:7;
then
A46: M is being_line by AFF_1:def 3;
A47: b9 in K by AFF_1:15;
then
A48: K<>M by A19,A29,A43,A33,AFF_1:21;
now
A49: now
p,q // a9,c9 by A25,A26,A34,AFF_1:5;
then
A50: c9,a9 // q,p by AFF_1:4;
A51: b,a // b,p by A21,AFF_1:def 1;
set D=Line(b,c);
A52: b in D by AFF_1:15;
D is being_line by A40,AFF_1:def 3;
then consider D9 such that
A53: c9 in D9 and
A54: D // D9 by AFF_1:49;
A55: D9 is being_line by A54,AFF_1:36;
A56: q in D by A23,AFF_1:def 2;
assume
A57: M<>P;
not D9 // P
proof
assume D9 // P;
then D // P by A54,AFF_1:44;
then q in P by A11,A52,A56,AFF_1:45;
hence contradiction by A4,A12,A46,A44,A32,A37,A57,AFF_1:18;
end;
then consider d such that
A58: d in D9 and
A59: d in P by A4,A55,AFF_1:58;
A60: c in D by AFF_1:15;
A61: d<>b9
proof
assume d=b9;
then M=D9 by A45,A46,A44,A33,A53,A55,A58,AFF_1:18;
then
A62: D=M by A32,A56,A54,AFF_1:45;
then LIN c,c9,b by A46,A33,A52,A60,AFF_1:21;
then
A63: b in C by A5,A13,A14,A20,AFF_1:25;
set N=Line(a,c);
set T=Line(b,a);
A64: b in T by AFF_1:15;
A65: c in N by AFF_1:15;
A66: a in T by AFF_1:15;
A67: N is being_line by A34,AFF_1:def 3;
A68: a in N by AFF_1:15;
A69: a<>a9
proof
assume a=a9;
then LIN a,c,c9 by A25,AFF_1:def 1;
then c9 in N by AFF_1:def 2;
then N=C by A5,A13,A14,A20,A67,A65,AFF_1:18;
hence contradiction by A13,A18,A63,A67,A68,AFF_1:21;
end;
A70: T is being_line & p in T by A21,A41,AFF_1:def 2,def 3;
A71: b<>b9
proof
A72: K<>T
proof
assume K=T;
then T=A by A3,A9,A29,A43,A66,A69,AFF_1:18;
hence contradiction by A3,A4,A6,A8,A10,A11,A16,A64,AFF_1:18;
end;
assume b=b9;
hence contradiction by A29,A47,A28,A35,A64,A70,A72,AFF_1:18;
end;
LIN c,c9,b9 by A46,A44,A33,A60,A62,AFF_1:21;
then b9 in C by A5,A13,A14,A20,AFF_1:25;
hence contradiction by A4,A5,A7,A11,A12,A63,A71,AFF_1:18;
end;
c9,d // q,b by A52,A56,A53,A54,A58,AFF_1:39;
then d,a9 // b,p by A1,A4,A11,A12,A42,A29,A46,A47,A43,A28,A44,A33,A32,A48
,A57,A59,A61,A50;
then
A73: b,a // d,a9 by A27,A51,AFF_1:5;
b,c // d,c9 by A52,A60,A53,A54,A58,AFF_1:39;
hence
thesis by A2,A3,A4,A5,A6,A8,A9,A10,A11,A13,A14,A15,A16,A18,A20,A25,A59
,A73;
end;
now
assume
A74: M=P;
LIN b,q,c by A23,AFF_1:6;
then c in P by A11,A46,A32,A30,A74,AFF_1:25;
then P=Line(c,c9) by A20,A46,A33,A74,AFF_1:57;
hence thesis by A5,A10,A13,A14,A20,AFF_1:57;
end;
hence thesis by A49;
end;
hence thesis;
end;
theorem
AP is satisfying_DES1_2 implies AP is satisfying_DES1_3
proof
assume
A1: AP is satisfying_DES1_2;
let A,P,C,o,a,a9,b,b9,c,c9,p,q;
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P<>A and
A6: P<>C and
A7: A<>C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: o in C and
A14: c in C and
A15: c9 in C and
A16: o<>a and
A17: o<>b and
A18: o<>c and
A19: p<>q and
A20: not LIN b,a,c and
A21: not LIN b9,a9,c9 and
A22: b<>b9 and
A23: a<>a9 and
A24: LIN b,a,p and
A25: LIN b9,a9,p and
A26: LIN b,c,q and
A27: LIN b9,c9,q and
A28: a,c // a9,c9 and
A29: a,c // p,q;
set D=Line(b,c), K=Line(b9,a9);
assume
A30: not thesis;
A31: not LIN o,c,a
proof
assume LIN o,c,a;
then a in C by A4,A13,A14,A18,AFF_1:25;
hence contradiction by A2,A4,A7,A8,A9,A13,A16,AFF_1:18;
end;
A32: c <>c9
proof
assume c =c9;
then
A33: c,a // c,a9 by A28,AFF_1:4;
LIN o,a,a9 by A2,A8,A9,A10,AFF_1:21;
hence contradiction by A23,A31,A33,AFF_1:14;
end;
a<>c by A20,AFF_1:7;
then
A34: a9,c9 // p,q by A28,A29,AFF_1:5;
A35: p<>b & p<>b9 & q<>b & q<>b9
proof
A36: now
assume
A37: b9=q;
( not LIN b9,c9,a9)& c9,a9 // q,p by A21,A34,AFF_1:4,6;
hence contradiction by A19,A25,A37,AFF_1:55;
end;
A38: now
assume
A39: b=q;
( not LIN b,c,a)& c,a // q,p by A20,A29,AFF_1:4,6;
hence contradiction by A19,A24,A39,AFF_1:55;
end;
assume not thesis;
hence contradiction by A20,A21,A26,A27,A29,A34,A38,A36,AFF_1:55;
end;
A40: b<>c by A20,AFF_1:7;
then
A41: D is being_line & c in D by AFF_1:24;
A42: b in D by A40,AFF_1:24;
then
A43: q in D by A26,A40,A41,AFF_1:25;
A44: now
assume not C // P;
then consider x such that
A45: x in C and
A46: x in P by A3,A4,AFF_1:58;
A47: x<>c
proof
A48: LIN q,b9,c9 & LIN q,b9,b9 by A27,AFF_1:6,7;
assume
A49: x=c;
then LIN b,c,b9 & LIN b,c,c by A3,A11,A12,A46,AFF_1:21;
then LIN q,b9,c by A26,A40,AFF_1:8;
then
A50: b9 in C by A4,A14,A15,A32,A35,A48,AFF_1:8,25;
then LIN c,c9,q by A3,A4,A6,A12,A14,A27,A46,A49,AFF_1:18;
then
A51: q in C by A4,A14,A15,A32,AFF_1:25;
c =b9 by A3,A4,A6,A12,A14,A46,A49,A50,AFF_1:18;
then C=D by A4,A14,A35,A41,A43,A51,AFF_1:18;
hence contradiction by A3,A4,A6,A11,A12,A22,A42,A50,AFF_1:18;
end;
A52: x<>b
proof
A53: LIN q,c9,b9 by A27,AFF_1:6;
assume
A54: x=b;
then q in C by A4,A14,A26,A40,A45,AFF_1:25;
then q=c9 or b9 in C by A4,A15,A53,AFF_1:25;
then c9,a9 // c9,p by A3,A4,A6,A11,A12,A22,A34,A45,A54,AFF_1:4,18;
then LIN c9,a9,p by AFF_1:def 1;
then
A55: LIN p,a9,c9 by AFF_1:6;
LIN p,a9,b9 & LIN p,a9,a9 by A25,AFF_1:6,7;
then p=a9 by A21,A55,AFF_1:8;
then LIN a,a9,b by A24,AFF_1:6;
then b in A by A2,A9,A10,A23,AFF_1:25;
hence contradiction by A2,A4,A7,A8,A13,A17,A45,A54,AFF_1:18;
end;
A56: c,a // q,p & c,a // c9,a9 by A28,A29,AFF_1:4;
( not LIN b,c,a)& not LIN b9,c9,a9 by A20,A21,AFF_1:6;
then x in A by A1,A2,A3,A4,A6,A9,A10,A11,A12,A14,A15,A19,A23,A24,A25,A26
,A27,A45,A46,A47,A52,A56;
hence contradiction by A2,A4,A7,A8,A13,A30,A45,A46,AFF_1:18;
end;
A57: a<>b by A20,AFF_1:7;
A58: a9<>b9 by A21,AFF_1:7;
then
A59: a9 in K by AFF_1:24;
A60: K is being_line & b9 in K by A58,AFF_1:24;
then
A61: p in K by A25,A58,A59,AFF_1:25;
A62: now
assume not P // A;
then consider x such that
A63: x in P and
A64: x in A by A2,A3,AFF_1:58;
A65: x<>b
proof
assume
A66: x=b;
then p in A by A2,A9,A24,A57,A64,AFF_1:25;
then a9,c9 // a9,q or b9 in A by A2,A10,A34,A60,A59,A61,AFF_1:18;
then LIN a9,c9,q by A2,A3,A5,A11,A12,A22,A64,A66,AFF_1:18,def 1;
then
A67: LIN q,c9,a9 by AFF_1:6;
LIN q,c9,b9 & LIN q,c9,c9 by A27,AFF_1:6,7;
then q=c9 by A21,A67,AFF_1:8;
then LIN c,c9,b by A26,AFF_1:6;
then b in C by A4,A14,A15,A32,AFF_1:25;
hence contradiction by A2,A4,A7,A8,A13,A17,A64,A66,AFF_1:18;
end;
x<>a
proof
assume x=a;
then p in P & K<>P by A2,A3,A5,A9,A10,A11,A23,A24,A57,A59,A63,AFF_1:18,25
;
hence contradiction by A3,A12,A35,A60,A61,AFF_1:18;
end;
then x in C by A1,A2,A3,A4,A5,A9,A10,A11,A12,A14,A15,A19,A20,A21,A24,A25
,A26,A27,A28,A29,A32,A63,A64,A65;
hence contradiction by A2,A4,A7,A8,A13,A30,A63,A64,AFF_1:18;
end;
not P // A or not C // P
proof
assume not thesis;
then C // A by AFF_1:44;
hence contradiction by A7,A8,A13,AFF_1:45;
end;
hence contradiction by A62,A44;
end;
theorem
AP is satisfying_DES1_2 implies AP is Desarguesian
proof
assume
A1: AP is satisfying_DES1_2;
let A,P,C,o,a,b,c,a9,b9,c9;
assume that
A2: o in A and
A3: o in P and
A4: o in C and
A5: o<>a and
A6: o<>b and
A7: o<>c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A<>P and
A18: A<>C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9;
now
A21: not LIN o,b,a & not LIN o,a,c
proof
A22: now
assume LIN o,a,c;
then c in A by A2,A5,A8,A14,AFF_1:25;
hence contradiction by A2,A4,A7,A12,A14,A16,A18,AFF_1:18;
end;
A23: now
assume LIN o,b,a;
then a in P by A3,A6,A10,A15,AFF_1:25;
hence contradiction by A2,A3,A5,A8,A14,A15,A17,AFF_1:18;
end;
assume not thesis;
hence thesis by A23,A22;
end;
A24: b=b9 implies thesis
proof
A25: LIN o,c,c9 by A4,A12,A13,A16,AFF_1:21;
A26: LIN o,a,a9 by A2,A8,A9,A14,AFF_1:21;
assume
A27: b=b9;
then b,a // b,a9 by A19,AFF_1:4;
then a,c // a,c9 by A20,A21,A26,AFF_1:14;
then c =c9 by A21,A25,AFF_1:14;
hence thesis by A27,AFF_1:2;
end;
A28: a9=o implies thesis
proof
assume
A29: a9=o;
LIN o,b,b9 & not LIN o,a,b by A3,A10,A11,A15,A21,AFF_1:6,21;
then
A30: o=b9 by A19,A29,AFF_1:55;
LIN o,c,c9 by A4,A12,A13,A16,AFF_1:21;
then o=c9 by A20,A21,A29,AFF_1:55;
hence thesis by A30,AFF_1:3;
end;
A31: c9=o implies thesis
proof
A32: c,a // c9,a9 by A20,AFF_1:4;
assume
A33: c9=o;
LIN o,a,a9 & not LIN o,c,a by A2,A8,A9,A14,A21,AFF_1:6,21;
hence thesis by A28,A33,A32,AFF_1:55;
end;
set K=Line(a,c);
A34: a in K by AFF_1:15;
A35: a<>c by A2,A4,A5,A8,A12,A14,A16,A18,AFF_1:18;
then
A36: K is being_line by AFF_1:def 3;
A37: c in K by AFF_1:15;
A38: a<>b by A2,A3,A5,A8,A10,A14,A15,A17,AFF_1:18;
A39: LIN a,b,c implies thesis
proof
consider N such that
A40: a9 in N and
A41: K // N by A36,AFF_1:49;
A42: N is being_line by A41,AFF_1:36;
a9,c9 // K by A20,A35,AFF_1:29,32;
then a9,c9 // N by A41,AFF_1:43;
then
A43: c9 in N by A40,A42,AFF_1:23;
assume LIN a,b,c;
then LIN a,c,b by AFF_1:6;
then
A44: b in K by AFF_1:def 2;
then K=Line(a,b) by A38,A36,A34,AFF_1:57;
then a9,b9 // K by A19,A38,AFF_1:29,32;
then a9,b9 // N by A41,AFF_1:43;
then b9 in N by A40,A42,AFF_1:23;
hence thesis by A37,A44,A41,A43,AFF_1:39;
end;
assume
A45: P<>C;
A46: now
set T=Line(b9,a9);
set D=Line(b,a);
set N=Line(a9,c9);
assume that
A47: o<>a9 and
A48: o<>b9 and
A49: o<>c9 and
A50: b<>b9 and
A51: not LIN a,b,c;
A52: c9 in N by AFF_1:15;
assume not b,c // b9,c9;
then consider q such that
A53: LIN b,c,q and
A54: LIN b9,c9,q by AFF_1:60;
consider M such that
A55: q in M and
A56: K // M by A36,AFF_1:49;
A57: M is being_line by A56,AFF_1:36;
not a,b // M
proof
assume a,b // M;
then a,b // K by A56,AFF_1:43;
then b in K by A36,A34,AFF_1:23;
hence contradiction by A36,A34,A37,A51,AFF_1:21;
end;
then consider p such that
A58: p in M and
A59: LIN a,b,p by A57,AFF_1:59;
A60: a9 in N by AFF_1:15;
A61: p<>q
proof
A62: LIN p,b,a & LIN p,b,b by A59,AFF_1:6,7;
assume
A63: p=q;
then LIN p,b,c by A53,AFF_1:6;
then p=b by A51,A62,AFF_1:8;
then LIN b,b9,c9 by A54,A63,AFF_1:6;
then c9 in P by A10,A11,A15,A50,AFF_1:25;
hence contradiction by A3,A4,A13,A15,A16,A45,A49,AFF_1:18;
end;
A64: c,a // q,p by A34,A37,A55,A56,A58,AFF_1:39;
A65: LIN b,a,p by A59,AFF_1:6;
A66: b9<>c9 by A3,A4,A11,A13,A15,A16,A45,A48,AFF_1:18;
A67: a9<>c9 by A2,A4,A9,A13,A14,A16,A18,A47,AFF_1:18;
then
A68: N is being_line by AFF_1:def 3;
A69: K // N by A20,A35,A67,AFF_1:37;
then
A70: N // M by A56,AFF_1:44;
A71: a9<>b9 by A2,A3,A9,A11,A14,A15,A17,A47,AFF_1:18;
A72: not LIN a9,b9,c9
proof
assume LIN a9,b9,c9;
then LIN a9,c9,b9 by AFF_1:6;
then b9 in N by AFF_1:def 2;
then a9,b9 // N by A68,A60,AFF_1:23;
then
A73: a9,b9 // K by A69,AFF_1:43;
a9,b9 // a,b by A19,AFF_1:4;
then a,b // K by A71,A73,AFF_1:32;
then b in K by A36,A34,AFF_1:23;
hence contradiction by A36,A34,A37,A51,AFF_1:21;
end;
not b9,p // N
proof
assume b9,p // N;
then b9,p // M by A70,AFF_1:43;
then p,b9 // M by AFF_1:34;
then
A74: b9 in M by A57,A58,AFF_1:23;
A75: now
assume
A76: b9<>q;
LIN b9,q,c9 by A54,AFF_1:6;
then c9 in M by A55,A57,A74,A76,AFF_1:25;
then a9 in N & b9 in N by A52,A70,A74,AFF_1:15,45;
hence contradiction by A68,A52,A72,AFF_1:21;
end;
now
assume b9=q;
then LIN b,b9,c by A53,AFF_1:6;
then c in P by A10,A11,A15,A50,AFF_1:25;
hence contradiction by A3,A4,A7,A12,A15,A16,A45,AFF_1:18;
end;
hence thesis by A75;
end;
then consider x such that
A77: x in N and
A78: LIN b9,p,x by A68,AFF_1:59;
set A9=Line(x,a);
A79: a<>a9
proof
assume
A80: a=a9;
( not LIN o,a,b)& LIN o,b,b9 by A3,A10,A11,A15,A21,AFF_1:6,21;
hence contradiction by A19,A50,A80,AFF_1:14;
end;
A81: x<>a
proof
assume x=a;
then a9 in K by A34,A60,A69,A77,AFF_1:45;
then A=K by A8,A9,A14,A36,A34,A79,AFF_1:18;
hence contradiction by A2,A4,A7,A12,A14,A16,A18,A37,AFF_1:18;
end;
then
A82: A9 is being_line by AFF_1:def 3;
A83: c <>c9
proof
assume c =c9;
then
A84: c,a // c,a9 by A20,AFF_1:4;
( not LIN o,c,a)& LIN o,a,a9 by A2,A8,A9,A14,A21,AFF_1:6,21;
hence contradiction by A79,A84,AFF_1:14;
end;
A85: not LIN b9,c9,x
proof
A86: now
A87: now
assume q=c9;
then LIN c,c9,b by A53,AFF_1:6;
then b in C by A12,A13,A16,A83,AFF_1:25;
hence contradiction by A3,A4,A6,A10,A15,A16,A45,AFF_1:18;
end;
assume c9=x;
then
A88: LIN b9,c9,p by A78,AFF_1:6;
LIN b9,c9,c9 by AFF_1:7;
then c9 in M by A66,A54,A55,A57,A58,A61,A88,AFF_1:8,25;
then
A89: q in N by A55,A52,A70,AFF_1:45;
LIN q,c9,b9 by A54,AFF_1:6;
then q=c9 or b9 in N by A68,A52,A89,AFF_1:25;
hence LIN b9,c9,a9 by A68,A60,A52,A87,AFF_1:21;
end;
assume LIN b9,c9,x;
then
A90: LIN c9,x,b9 by AFF_1:6;
A91: LIN c9,x,a9 & LIN c9,x,c9 by A68,A60,A52,A77,AFF_1:21;
then LIN c9,a9,b9 by A90,A86,AFF_1:6,8;
then c9,a9 // c9,b9 by AFF_1:def 1;
then a9,c9 // b9,c9 by AFF_1:4;
then
A92: a,c // b9,c9 by A20,A67,AFF_1:5;
c9=x or LIN b9,c9,a9 by A90,A91,AFF_1:8;
then b9,c9 // b9,a9 by A86,AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
then b9,c9 // a,b by A19,A71,AFF_1:5;
then a,c // a,b by A66,A92,AFF_1:5;
then LIN a,c,b by AFF_1:def 1;
hence contradiction by A51,AFF_1:6;
end;
A93: x in A9 & a in A9 by AFF_1:15;
A<>K by A2,A4,A7,A12,A14,A16,A18,A37,AFF_1:18;
then
A94: A <> N by A8,A34,A69,AFF_1:45;
A95: not LIN b,c,a by A51,AFF_1:6;
A96: p in D by A59,AFF_1:def 2;
A97: D is being_line & b in D by A38,AFF_1:15,def 3;
A98: LIN b9,x,p by A78,AFF_1:6;
c,a // c9,x by A34,A37,A52,A69,A77,AFF_1:39;
then o in A9 by A1,A3,A4,A6,A7,A10,A11,A12,A13,A15,A16,A45,A53,A54,A98
,A81,A82,A93,A61,A85,A64,A95,A65;
then x in A by A2,A5,A8,A14,A82,A93,AFF_1:18;
then x=a9 by A9,A14,A68,A60,A77,A94,AFF_1:18;
then
A99: a9 in T & p in T by A98,AFF_1:15,def 2;
D // T by A19,A38,A71,AFF_1:37;
then a in D & a9 in D by A96,A99,AFF_1:15,45;
then b in A by A8,A9,A14,A79,A97,AFF_1:18;
hence contradiction by A2,A3,A6,A10,A14,A15,A17,AFF_1:18;
end;
b9=o implies thesis
proof
assume
A100: b9=o;
LIN o,a,a9 & b,a // b9,a9 by A2,A8,A9,A14,A19,AFF_1:4,21;
hence thesis by A21,A28,A100,AFF_1:55;
end;
hence thesis by A28,A31,A39,A24,A46;
end;
hence thesis by A10,A11,A12,A13,A15,AFF_1:51;
end;
theorem
AP is satisfying_DES2_1 implies AP is satisfying_DES2
proof
assume
A1: AP is satisfying_DES2_1;
let A,P,C,a,a9,b,b9,c,c9,p,q;
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: A<>P and
A6: A<>C and
A7: P<>C and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p<>q and
A19: a<>a9 and
A20: LIN b,a,p and
A21: LIN b9,a9,p and
A22: LIN b,c,q & LIN b9,c9,q and
A23: a,c // a9,c9;
A24: P // C by A14,A15,AFF_1:44;
set P9=Line(b9,a9);
A25: p in P9 by A21,AFF_1:def 2;
a9<>b9 by A17,AFF_1:7;
then
A26: P9 is being_line by AFF_1:def 3;
set K=Line(a,c), N=Line(a9,c9), D=Line(b,c), T=Line(b9,c9);
A27: q in D & q in T by A22,AFF_1:def 2;
A28: c9 in N by AFF_1:15;
b<>c by A16,AFF_1:7;
then
A29: D is being_line by AFF_1:def 3;
b9<>c9 by A17,AFF_1:7;
then
A30: T is being_line by AFF_1:def 3;
A31: a<>c by A16,AFF_1:7;
then
A32: K is being_line by AFF_1:def 3;
A33: a9<>c9 by A17,AFF_1:7;
then
A34: N is being_line by AFF_1:def 3;
then consider M such that
A35: p in M and
A36: N // M by AFF_1:49;
A37: K // N by A23,A31,A33,AFF_1:37;
then
A38: K // M by A36,AFF_1:44;
A39: c in D by AFF_1:15;
A40: b in D by AFF_1:15;
set A9=Line(b,a);
A41: p in A9 by A20,AFF_1:def 2;
a<>b by A16,AFF_1:7;
then
A42: A9 is being_line by AFF_1:def 3;
A43: c9 in T by AFF_1:15;
A44: b9 in T by AFF_1:15;
A45: a9 in N by AFF_1:15;
A46: a in K by AFF_1:15;
A47: a9 in P9 by AFF_1:15;
A48: b9 in P9 by AFF_1:15;
A49: a in A9 by AFF_1:15;
A50: b in A9 by AFF_1:15;
A51: c in K by AFF_1:15;
then
A52: K<>A by A6,A12,A15,AFF_1:45;
A53: c <>c9
proof
assume c =c9;
then K=N by A51,A28,A37,AFF_1:45;
hence contradiction by A2,A8,A9,A19,A32,A46,A45,A52,AFF_1:18;
end;
A54: D<>T
proof
assume D=T;
then D=C by A4,A12,A13,A29,A39,A43,A53,AFF_1:18;
hence contradiction by A7,A10,A24,A40,AFF_1:45;
end;
A55: b<>b9
proof
A56: A9<>P9
proof
assume A9=P9;
then A9=A by A2,A8,A9,A19,A42,A49,A47,AFF_1:18;
hence contradiction by A5,A10,A14,A50,AFF_1:45;
end;
assume
A57: b=b9;
then b9=q by A29,A30,A40,A44,A27,A54,AFF_1:18;
hence contradiction by A18,A42,A26,A50,A41,A48,A25,A57,A56,AFF_1:18;
end;
A58: M is being_line by A36,AFF_1:36;
A59: now
assume not T // M;
then consider x such that
A60: x in T and
A61: x in M by A30,A58,AFF_1:58;
A62: p<>x
proof
assume p=x;
then p=b9 or T=P9 by A30,A44,A26,A48,A25,A60,AFF_1:18;
then LIN b,b9,a or c9 in P9 by A42,A50,A49,A41,AFF_1:15,21;
then a in P by A3,A10,A11,A17,A55,AFF_1:25,def 2;
hence contradiction by A5,A8,A14,AFF_1:45;
end;
not b,x // C
proof
assume
A63: b,x // C;
C // P by A14,A15,AFF_1:44;
then b,x // P by A63,AFF_1:43;
then x in P by A3,A10,AFF_1:23;
then b9 in M or c9 in P by A3,A11,A30,A44,A43,A60,A61,AFF_1:18;
then b9=p or M=P9 by A7,A13,A24,A26,A48,A25,A35,A58,AFF_1:18,45;
then LIN b,b9,a or N // P9 by A20,A36,AFF_1:6;
then a in P or N=P9 by A3,A10,A11,A45,A47,A55,AFF_1:25,45;
hence contradiction by A5,A8,A14,A17,A28,AFF_1:45,def 2;
end;
then consider y such that
A64: y in C and
A65: LIN b,x,y by A4,AFF_1:59;
A66: LIN b,y,x by A65,AFF_1:6;
A67: not LIN b,a,y
proof
A68: now
assume x=p;
then p=b9 or T=P9 by A30,A44,A26,A48,A25,A60,AFF_1:18;
then LIN b,b9,a or c9 in P9 by A42,A50,A49,A41,AFF_1:15,21;
then a in P by A3,A10,A11,A17,A55,AFF_1:25,def 2;
hence contradiction by A5,A8,A14,AFF_1:45;
end;
assume LIN b,a,y;
then
A69: LIN b,y,a by AFF_1:6;
LIN b,y,b by AFF_1:7;
then b=y or LIN a,b,x by A66,A69,AFF_1:8;
then x in A9 by A7,A10,A24,A64,AFF_1:45,def 2;
then x=p or A9=M by A42,A41,A35,A58,A61,AFF_1:18;
then K=A9 by A46,A49,A38,A68,AFF_1:45;
hence contradiction by A16,A51,AFF_1:def 2;
end;
LIN b9,c9,x & a9,c9 // p,x by A30,A45,A28,A44,A43,A35,A36,A60,A61,AFF_1:21
,39;
then a9,c9 // a,y by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A13,A14,A15,A17,A20
,A21,A64,A66,A67,A62;
then a,c // a,y by A23,A33,AFF_1:5;
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 A4,A12,A32,A51,A64,AFF_1:18;
then a in C or LIN b,c,x by A65,AFF_1:6,15;
then x in D by A6,A8,A15,AFF_1:45,def 2;
then q in M or c9 in D by A29,A30,A43,A27,A60,A61,AFF_1:18;
then a,c // p,q or LIN c,c9,b by A29,A46,A51,A40,A39,A35,A38,AFF_1:21,39;
then a,c // p,q or b in C by A4,A12,A13,A53,AFF_1:25;
hence thesis by A7,A10,A24,AFF_1:45;
end;
A70: now
assume not M // D;
then consider x such that
A71: x in M and
A72: x in D by A29,A58,AFF_1:58;
A73: p<>x
proof
assume p=x;
then p=b or D=A9 by A29,A40,A42,A50,A41,A72,AFF_1:18;
then LIN b,b9,a9 or c in A9 by A26,A48,A47,A25,AFF_1:15,21;
then a9 in P by A3,A10,A11,A16,A55,AFF_1:25,def 2;
hence contradiction by A5,A9,A14,AFF_1:45;
end;
not b9,x // C
proof
A74: now
assume b=p;
then LIN b,b9,a9 by A26,A48,A47,A25,AFF_1:21;
then a9 in P by A3,A10,A11,A55,AFF_1:25;
hence contradiction by A5,A9,A14,AFF_1:45;
end;
assume
A75: b9,x // C;
C // P by A14,A15,AFF_1:44;
then b9,x // P by A75,AFF_1:43;
then x in P by A3,A11,AFF_1:23;
then x=b or D=P by A3,A10,A29,A40,A72,AFF_1:18;
then b=p or M=A9 by A7,A12,A24,A39,A42,A50,A41,A35,A58,A71,AFF_1:18,45;
then b in K by A46,A50,A49,A38,A74,AFF_1:45;
hence contradiction by A16,A32,A46,A51,AFF_1:21;
end;
then consider y such that
A76: y in C and
A77: LIN b9,x,y by A4,AFF_1:59;
A78: LIN b9,y,x by A77,AFF_1:6;
A79: not LIN b9,a9,y
proof
A80: now
assume x=p;
then p=b or D=A9 by A29,A40,A42,A50,A41,A72,AFF_1:18;
then LIN b,b9,a9 or c in A9 by A26,A48,A47,A25,AFF_1:15,21;
then a9 in P by A3,A10,A11,A16,A55,AFF_1:25,def 2;
hence contradiction by A5,A9,A14,AFF_1:45;
end;
assume LIN b9,a9,y;
then
A81: LIN b9,y,a9 by AFF_1:6;
LIN b9,y,b9 by AFF_1:7;
then b9=y or LIN a9,b9,x by A78,A81,AFF_1:8;
then x in P9 by A7,A11,A24,A76,AFF_1:45,def 2;
then x=p or P9=M by A26,A25,A35,A58,A71,AFF_1:18;
then N=P9 by A45,A47,A36,A80,AFF_1:45;
hence contradiction by A17,A28,AFF_1:def 2;
end;
LIN b,c,x & a,c // p,x by A29,A46,A51,A40,A39,A35,A38,A71,A72,AFF_1:21,39;
then a,c // a9,y by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A14,A15,A16,A20
,A21,A76,A78,A79,A73;
then a9,y // a9,c9 by A23,A31,AFF_1:5;
then LIN a9,y,c9 by AFF_1:def 1;
then LIN a9,c9,y by AFF_1:6;
then y in N by AFF_1:def 2;
then N=C or y=c9 by A4,A13,A34,A28,A76,AFF_1:18;
then a9 in C or LIN b9,c9,x by A77,AFF_1:6,15;
then x in T by A6,A9,A15,AFF_1:45,def 2;
then q in M or c9 in D by A29,A30,A43,A27,A71,A72,AFF_1:18;
then a,c // p,q or LIN c,c9,b by A29,A46,A51,A40,A39,A35,A38,AFF_1:21,39;
then a,c // p,q or b in C by A4,A12,A13,A53,AFF_1:25;
hence thesis by A7,A10,A24,AFF_1:45;
end;
not M // D or not T // M
proof
assume not thesis;
then T // D by AFF_1:44;
hence contradiction by A27,A54,AFF_1:45;
end;
hence thesis by A70,A59;
end;
theorem
AP is satisfying_DES2_1 iff AP is satisfying_DES2_3
proof
A1: AP is satisfying_DES2_1 implies AP is satisfying_DES2_3
proof
assume
A2: AP is satisfying_DES2_1;
thus AP is satisfying_DES2_3
proof
let A,P,C,a,a9,b,b9,c,c9,p,q;
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: A<>P and
A7: A<>C and
A8: P<>C and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A // P and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p<>q and
A19: c <>c9 and
A20: LIN b,a,p and
A21: LIN b9,a9,p and
A22: LIN b,c,q and
A23: LIN b9,c9,q and
A24: a,c // a9,c9 and
A25: a,c // p,q;
now
set A9=Line(a,c), P9=Line(p,q), C9=Line(a9,c9);
A26: LIN p,a9,b9 by A21,AFF_1:6;
A27: a<>c by A16,AFF_1:7;
then
A28: A9 is being_line & a in A9 by AFF_1:24;
A29: q<>c
proof
assume
A30: q=c;
then c,p // c,a by A25,AFF_1:4;
then LIN c,p,a by AFF_1:def 1;
then
A31: LIN p,a,c by AFF_1:6;
LIN p,a,b & LIN p,a,a by A20,AFF_1:6,7;
then a=p by A16,A31,AFF_1:8;
then LIN a,a9,b9 by A21,AFF_1:6;
then b9 in A or a=a9 by A3,A9,A10,AFF_1:25;
then a9,c9 // a9,c by A6,A12,A15,A24,AFF_1:4,45;
then LIN a9,c9,c by AFF_1:def 1;
then LIN c,c9,a9 by AFF_1:6;
then
A32: a9 in C by A5,A13,A14,A19,AFF_1:25;
LIN c,c9,b9 by A23,A30,AFF_1:6;
then b9 in C by A5,A13,A14,A19,AFF_1:25;
hence contradiction by A5,A14,A17,A32,AFF_1:21;
end;
A33: a<>p
proof
assume a=p;
then LIN a,c,q by A25,AFF_1:def 1;
then
A34: LIN c,q,a by AFF_1:6;
LIN c,q,b & LIN c,q,c by A22,AFF_1:6,7;
hence contradiction by A16,A29,A34,AFF_1:8;
end;
A35: a<>a9
proof
A36: LIN p,a,b & LIN p,a,a by A20,AFF_1:6,7;
assume
A37: a=a9;
then LIN a,c,c9 by A24,AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then
A38: a in C by A5,A13,A14,A19,AFF_1:25;
LIN p,a,b9 by A21,A37,AFF_1:6;
then b=b9 or a in P by A4,A11,A12,A33,A36,AFF_1:8,25;
then
A39: LIN q,b,c9 by A6,A9,A15,A23,AFF_1:6,45;
LIN q,b,c & LIN q,b,b by A22,AFF_1:6,7;
then
A40: q=b or LIN c,c9,b by A39,AFF_1:8;
not b in C by A5,A13,A16,A38,AFF_1:21;
then LIN p,q,a by A5,A13,A14,A19,A20,A40,AFF_1:6,25;
then p,q // p,a by AFF_1:def 1;
then a,c // p,a by A18,A25,AFF_1:5;
then a,c // a,p by AFF_1:4;
then LIN a,c,p by AFF_1:def 1;
then
A41: p in C by A5,A13,A27,A38,AFF_1:25;
LIN p,a,b by A20,AFF_1:6;
then b in C by A5,A33,A38,A41,AFF_1:25;
hence contradiction by A5,A13,A16,A38,AFF_1:21;
end;
A42: b<>b9
proof
A43: p,q // c,a by A25,AFF_1:4;
A44: LIN q,b,c & LIN q,b,b by A22,AFF_1:6,7;
A45: LIN p,b,a & LIN p,b,b by A20,AFF_1:6,7;
assume
A46: b=b9;
then LIN p,b,a9 by A21,AFF_1:6;
then
A47: p=b or b in A by A3,A9,A10,A35,A45,AFF_1:8,25;
LIN q,b,c9 by A23,A46,AFF_1:6;
then b=q or LIN c,c9,b by A44,AFF_1:8;
then
A48: b in C by A5,A6,A11,A13,A14,A15,A18,A19,A47,AFF_1:25,45;
then q in C by A5,A6,A11,A13,A15,A16,A20,A22,A47,AFF_1:25,45;
then a in C by A5,A6,A11,A13,A15,A18,A47,A48,A43,AFF_1:45,48;
hence contradiction by A5,A13,A16,A48,AFF_1:21;
end;
then
A49: a9,a // b9,b by A3,A4,A9,A10,A11,A12,A15,A35,AFF_1:38;
A50: a9<>c9 by A17,AFF_1:7;
then
A51: C9 is being_line by AFF_1:24;
A52: c9 in C9 by A50,AFF_1:24;
A53: LIN p,a,b by A20,AFF_1:6;
A54: not LIN p,a9,a
proof
assume LIN p,a9,a;
then
A55: LIN p,a,a9 by AFF_1:6;
LIN p,a,a by AFF_1:7;
then b in A by A3,A9,A10,A33,A35,A53,A55,AFF_1:8,25;
hence contradiction by A6,A11,A15,AFF_1:45;
end;
A56: LIN q,c9,b9 by A23,AFF_1:6;
A57: a9 in C9 by A50,AFF_1:24;
A58: c in A9 by A27,AFF_1:24;
then
A59: C9 // A9 by A24,A27,A50,A51,A28,A57,A52,AFF_1:38;
A60: A9<>C9
proof
assume
A61: A9=C9;
then LIN a,a9,c9 by A28,A57,A52,AFF_1:21;
then
A62: c9 in A by A3,A9,A10,A35,AFF_1:25;
LIN a,a9,c by A28,A58,A57,A61,AFF_1:21;
then c in A by A3,A9,A10,A35,AFF_1:25;
hence contradiction by A3,A5,A7,A13,A14,A19,A62,AFF_1:18;
end;
A63: LIN q,c,b by A22,AFF_1:6;
A64: p in P9 by A18,AFF_1:24;
A65: A9<>P9
proof
assume A9=P9;
then
A66: LIN p,a,c & LIN p,a,a by A28,A58,A64,AFF_1:21;
LIN p,a,b by A20,AFF_1:6;
hence contradiction by A16,A33,A66,AFF_1:8;
end;
A67: P9 is being_line by A18,AFF_1:24;
A68: P9<>C9
proof
assume P9=C9;
then
A69: LIN p,a9,c9 & LIN p,a9,a9 by A67,A64,A57,A52,AFF_1:21;
LIN p,a9,b9 by A21,AFF_1:6;
then p=a9 by A17,A69,AFF_1:8;
then LIN a,a9,b by A20,AFF_1:6;
then b in A by A3,A9,A10,A35,AFF_1:25;
hence contradiction by A6,A11,A15,AFF_1:45;
end;
A70: a9,c9 // p,q by A24,A25,A27,AFF_1:5;
A71: not LIN q,c9,c
proof
A72: now
assume q=c9;
then c9,a9 // c9,p by A70,AFF_1:4;
then LIN c9,a9,p by AFF_1:def 1;
then p in C9 by A50,A51,A57,A52,AFF_1:25;
then p=a9 or b9 in C9 by A51,A57,A26,AFF_1:25;
then LIN a,a9,b by A17,A20,A51,A57,A52,AFF_1:6,21;
then b in A by A3,A9,A10,A35,AFF_1:25;
hence contradiction by A6,A11,A15,AFF_1:45;
end;
assume
A73: LIN q,c9,c;
LIN q,c9,c9 by AFF_1:7;
then
A74: b9 in C by A5,A13,A14,A19,A56,A73,A72,AFF_1:8,25;
A75: LIN q,c,c by AFF_1:7;
LIN q,c,c9 by A73,AFF_1:6;
then b in C by A5,A13,A14,A19,A29,A63,A75,AFF_1:8,25;
hence contradiction by A4,A5,A8,A11,A12,A42,A74,AFF_1:18;
end;
A76: q in P9 by A18,AFF_1:24;
then C9 // P9 by A18,A50,A67,A51,A64,A57,A52,A70,AFF_1:38;
then a9,a // c9,c by A2,A67,A51,A28,A58,A64,A76,A57,A52,A42,A65,A60,A68
,A59,A49,A53,A26,A63,A56,A54,A71;
hence thesis by A3,A5,A9,A10,A13,A14,A19,A35,AFF_1:38;
end;
hence thesis;
end;
end;
AP is satisfying_DES2_3 implies AP is satisfying_DES2_1
proof
assume
A77: AP is satisfying_DES2_3;
thus AP is satisfying_DES2_1
proof
let A,P,C,a,a9,b,b9,c,c9,p,q;
assume that
A78: A is being_line and
A79: P is being_line and
A80: C is being_line and
A81: A<>P and
A<>C and
A82: P<>C and
A83: a in A and
A84: a9 in A and
A85: b in P and
A86: b9 in P and
A87: c in C and
A88: c9 in C and
A89: A // P and
A90: A // C and
A91: not LIN b,a,c and
A92: not LIN b9,a9,c9 and
A93: p<>q and
A94: LIN b,a,p and
A95: LIN b9,a9,p and
A96: LIN b,c,q and
A97: LIN b9,c9,q and
A98: a,c // p,q;
A99: C // P by A89,A90,AFF_1:44;
then
A100: c,c9 // b,b9 by A85,A86,A87,A88,AFF_1:39;
assume
A101: not thesis;
A102: q<>c
proof
assume
A103: q=c;
then c,p // c,a by A98,AFF_1:4;
then LIN c,p,a by AFF_1:def 1;
then
A104: LIN p,a,c by AFF_1:6;
LIN p,a,b & LIN p,a,a by A94,AFF_1:6,7;
then a=p by A91,A104,AFF_1:8;
then LIN a,a9,b9 by A95,AFF_1:6;
then
A105: b9 in A or a=a9 by A78,A83,A84,AFF_1:25;
LIN c,c9,b9 by A97,A103,AFF_1:6;
then c =c9 or b9 in C by A80,A87,A88,AFF_1:25;
hence contradiction by A81,A82,A86,A89,A101,A99,A105,AFF_1:2,45;
end;
A106: a<>p
proof
assume a=p;
then LIN a,c,q by A98,AFF_1:def 1;
then
A107: LIN c,q,a by AFF_1:6;
LIN c,q,b & LIN c,q,c by A96,AFF_1:6,7;
hence contradiction by A91,A102,A107,AFF_1:8;
end;
A108: a<>a9
proof
A109: LIN p,a,b & LIN p,a,a by A94,AFF_1:6,7;
assume
A110: a=a9;
then LIN p,a,b9 by A95,AFF_1:6;
then a in P or b=b9 by A79,A85,A86,A106,A109,AFF_1:8,25;
then
A111: LIN b,q,c9 by A81,A83,A89,A97,AFF_1:6,45;
LIN b,q,c & LIN b,q,b by A96,AFF_1:6,7;
then b=q or c =c9 or b in C by A80,A87,A88,A111,AFF_1:8,25;
then LIN p,q,a by A82,A85,A94,A101,A99,A110,AFF_1:2,6,45;
then p,q // p,a by AFF_1:def 1;
then a,c // p,a by A93,A98,AFF_1:5;
then a,c // a,p by AFF_1:4;
then LIN a,c,p by AFF_1:def 1;
then
A112: LIN p,a,c by AFF_1:6;
LIN p,a,b & LIN p,a,a by A94,AFF_1:6,7;
hence contradiction by A91,A106,A112,AFF_1:8;
end;
A113: not LIN p,a,a9
proof
assume
A114: LIN p,a,a9;
LIN p,a,b & LIN p,a,a by A94,AFF_1:6,7;
then b in A by A78,A83,A84,A106,A108,A114,AFF_1:8,25;
hence contradiction by A81,A85,A89,AFF_1:45;
end;
set A9=Line(a,c), P9=Line(p,q), C9=Line(a9,c9);
A115: a<>c by A91,AFF_1:7;
then
A116: A9 is being_line by AFF_1:24;
A117: c,c9 // a,a9 & LIN q,c,b by A83,A84,A87,A88,A90,A96,AFF_1:6,39;
A118: LIN p,a9,b9 by A95,AFF_1:6;
A119: a in A9 & c in A9 by A115,AFF_1:24;
A120: b<>b9
proof
assume b=b9;
then
A121: LIN b,p,a9 by A95,AFF_1:6;
LIN b,p,a & LIN b,p,b by A94,AFF_1:6,7;
then
A122: b=p or b in A by A78,A83,A84,A108,A121,AFF_1:8,25;
then LIN p,q,c by A81,A85,A89,A96,AFF_1:6,45;
then p,q // p,c by AFF_1:def 1;
then a,c // p,c by A93,A98,AFF_1:5;
then c,a // c,p by AFF_1:4;
then LIN c,a,p by AFF_1:def 1;
hence contradiction by A81,A85,A89,A91,A122,AFF_1:6,45;
end;
A123: not LIN q,c,c9
proof
assume
A124: LIN q,c,c9;
LIN q,c,b & LIN q,c,c by A96,AFF_1:6,7;
then c =c9 or b in C by A80,A87,A88,A102,A124,AFF_1:8,25;
then
A125: LIN q,c,b9 by A82,A85,A97,A99,AFF_1:6,45;
LIN q,c,b & LIN q,c,c by A96,AFF_1:6,7;
then c in P by A79,A85,A86,A102,A120,A125,AFF_1:8,25;
hence contradiction by A82,A87,A99,AFF_1:45;
end;
A126: LIN q,c9,b9 & LIN p,a,b by A94,A97,AFF_1:6;
A127: a9<>c9 by A92,AFF_1:7;
then
A128: C9 is being_line by AFF_1:24;
A129: p in P9 by A93,AFF_1:24;
A130: A9<>P9
proof
assume A9=P9;
then
A131: LIN p,a,c & LIN p,a,a by A116,A119,A129,AFF_1:21;
LIN p,a,b by A94,AFF_1:6;
hence contradiction by A91,A106,A131,AFF_1:8;
end;
A132: P9 is being_line & q in P9 by A93,AFF_1:24;
then
A133: A9 // P9 by A93,A98,A115,A116,A119,A129,AFF_1:38;
A134: a9 in C9 & c9 in C9 by A127,AFF_1:24;
then A9<>C9 by A101,A116,A119,AFF_1:51;
then A9 // C9 by A77,A127,A116,A128,A119,A129,A132,A134,A100,A133,A130
,A120,A123,A113,A117,A126,A118;
hence contradiction by A101,A119,A134,AFF_1:39;
end;
end;
hence thesis by A1;
end;
theorem
AP is satisfying_DES2 iff AP is satisfying_DES2_2
proof
A1: AP is satisfying_DES2 implies AP is satisfying_DES2_2
proof
assume
A2: AP is satisfying_DES2;
thus AP is satisfying_DES2_2
proof
let A,P,C,a,a9,b,b9,c,c9,p,q;
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: A<>P and
A7: A<>C and
A8: P<>C and
A9: a in A & a9 in A and
A10: b in P & b9 in P and
A11: c in C and
A12: c9 in C and
A13: A // C and
A14: not LIN b,a,c and
A15: not LIN b9,a9,c9 and
A16: p<>q and
A17: a<>a9 and
A18: LIN b,a,p and
A19: LIN b9,a9,p and
A20: LIN b,c,q and
A21: LIN b9,c9,q and
A22: a,c // a9,c9 and
A23: a,c // p,q;
A24: LIN q,c9,b9 by A21,AFF_1:6;
A25: c <>c9
proof
assume c =c9;
then c,a // c,a9 by A22,AFF_1:4;
then LIN c,a,a9 by AFF_1:def 1;
then LIN a,a9,c by AFF_1:6;
then c in A by A3,A9,A17,AFF_1:25;
hence contradiction by A7,A11,A13,AFF_1:45;
end;
A26: b<>b9
proof
A27: now
assume that
A28: b=p and
b in C;
LIN p,q,c by A20,A28,AFF_1:6;
then p,q // p,c by AFF_1:def 1;
then a,c // p,c by A16,A23,AFF_1:5;
then c,a // c,p by AFF_1:4;
then LIN c,a,p by AFF_1:def 1;
hence contradiction by A14,A28,AFF_1:6;
end;
A29: LIN b,p,a & LIN b,p,b by A18,AFF_1:6,7;
assume
A30: b=b9;
then LIN b,p,a9 by A19,AFF_1:6;
then
A31: b=p or b in A by A3,A9,A17,A29,AFF_1:8,25;
A32: LIN b,q,c & LIN b,q,b by A20,AFF_1:6,7;
LIN b,q,c9 by A21,A30,AFF_1:6;
then
A33: b=q or b in C by A5,A11,A12,A25,A32,AFF_1:8,25;
then LIN q,p,a by A7,A13,A18,A31,A27,AFF_1:6,45;
then q,p // q,a by AFF_1:def 1;
then p,q // q,a by AFF_1:4;
then a,c // q,a by A16,A23,AFF_1:5;
then a,c // a,q by AFF_1:4;
then LIN a,c,q by AFF_1:def 1;
hence contradiction by A7,A13,A14,A31,A33,A27,AFF_1:6,45;
end;
A34: a<>p
proof
assume
A35: a=p;
then LIN a,c,q by A23,AFF_1:def 1;
then
A36: LIN c,q,a by AFF_1:6;
LIN c,q,b & LIN c,q,c by A20,AFF_1:6,7;
then q=c by A14,A36,AFF_1:8;
then LIN c,c9,b9 by A21,AFF_1:6;
then
A37: c =c9 or b9 in C by A5,A11,A12,AFF_1:25;
LIN a,a9,b9 by A19,A35,AFF_1:6;
then b9 in A by A3,A9,A17,AFF_1:25;
then c,a // c,a9 by A7,A13,A22,A37,AFF_1:4,45;
then LIN c,a,a9 by AFF_1:def 1;
then LIN a,a9,c by AFF_1:6;
then c in A by A3,A9,A17,AFF_1:25;
hence contradiction by A7,A11,A13,AFF_1:45;
end;
A38: q<>c
proof
assume q=c;
then c,p // c,a by A23,AFF_1:4;
then LIN c,p,a by AFF_1:def 1;
then
A39: LIN p,a,c by AFF_1:6;
LIN p,a,b & LIN p,a,a by A18,AFF_1:6,7;
hence contradiction by A14,A34,A39,AFF_1:8;
end;
A40: LIN q,c,b by A20,AFF_1:6;
set A9=Line(a,c), P9=Line(p,q), C9=Line(a9,c9);
A41: a<>c by A14,AFF_1:7;
then
A42: c in A9 by AFF_1:24;
A43: a9<>p
proof
assume
A44: a9=p;
a9,c9 // p,q by A22,A23,A41,AFF_1:5;
then LIN a9,c9,q by A44,AFF_1:def 1;
then
A45: LIN c9,q,a9 by AFF_1:6;
LIN c9,q,b9 & LIN c9,q,c9 by A21,AFF_1:6,7;
then q=c9 by A15,A45,AFF_1:8;
then LIN c,c9,b by A20,AFF_1:6;
then
A46: b in C by A5,A11,A12,A25,AFF_1:25;
LIN a,a9,b by A18,A44,AFF_1:6;
then b in A by A3,A9,A17,AFF_1:25;
hence contradiction by A7,A13,A46,AFF_1:45;
end;
A47: c9<>q
proof
assume c9=q;
then a9,c9 // p,c9 by A22,A23,A41,AFF_1:5;
then c9,a9 // c9,p by AFF_1:4;
then LIN c9,a9,p by AFF_1:def 1;
then
A48: LIN p,a9,c9 by AFF_1:6;
LIN p,a9,b9 & LIN p,a9,a9 by A19,AFF_1:6,7;
hence contradiction by A15,A43,A48,AFF_1:8;
end;
A49: not LIN q,c9,c
proof
A50: LIN q,c,c by AFF_1:7;
assume
A51: LIN q,c9,c;
LIN q,c9,c9 by AFF_1:7;
then
A52: b9 in C by A5,A11,A12,A25,A47,A24,A51,AFF_1:8,25;
LIN q,c,c9 by A51,AFF_1:6;
then b in C by A5,A11,A12,A38,A25,A40,A50,AFF_1:8,25;
hence contradiction by A4,A5,A8,A10,A26,A52,AFF_1:18;
end;
A53: LIN p,a,b by A18,AFF_1:6;
A54: LIN p,a9,b9 by A19,AFF_1:6;
A55: not LIN p,a9,a
proof
A56: LIN p,a,a by AFF_1:7;
assume
A57: LIN p,a9,a;
LIN p,a9,a9 by AFF_1:7;
then
A58: b9 in A by A3,A9,A17,A43,A54,A57,AFF_1:8,25;
LIN p,a,a9 by A57,AFF_1:6;
then b in A by A3,A9,A17,A34,A53,A56,AFF_1:8,25;
hence contradiction by A3,A4,A6,A10,A26,A58,AFF_1:18;
end;
A59: a9,a // c9,c by A9,A11,A12,A13,AFF_1:39;
A60: q in P9 by A16,AFF_1:24;
A61: a9<>c9 by A15,AFF_1:7;
then
A62: a9 in C9 by AFF_1:24;
A63: A9 is being_line & a in A9 by A41,AFF_1:24;
A64: C9<>A9
proof
assume C9=A9;
then LIN a,a9,c by A63,A42,A62,AFF_1:21;
then c in A by A3,A9,A17,AFF_1:25;
hence contradiction by A7,A11,A13,AFF_1:45;
end;
A65: p in P9 by A16,AFF_1:24;
A66: P9<>A9
proof
assume P9=A9;
then
A67: LIN p,a,c & LIN p,a,a by A63,A42,A65,AFF_1:21;
LIN p,a,b by A18,AFF_1:6;
hence contradiction by A14,A34,A67,AFF_1:8;
end;
A68: c9 in C9 by A61,AFF_1:24;
A69: P9 is being_line by A16,AFF_1:24;
A70: C9<>P9
proof
assume C9=P9;
then
A71: LIN p,a9,c9 & LIN p,a9,a9 by A69,A65,A62,A68,AFF_1:21;
LIN p,a9,b9 by A19,AFF_1:6;
hence contradiction by A15,A43,A71,AFF_1:8;
end;
A72: C9 is being_line by A61,AFF_1:24;
a9,c9 // p,q by A22,A23,A41,AFF_1:5;
then
A73: C9 // P9 by A16,A61,A69,A72,A65,A60,A62,A68,AFF_1:38;
C9 // A9 by A22,A41,A61,A72,A63,A42,A62,A68,AFF_1:38;
then a9,a // b9,b by A2,A61,A26,A69,A72,A63,A42,A65,A60,A62,A68,A73,A64
,A70,A66,A54,A53,A24,A40,A55,A49,A59;
hence thesis by A3,A4,A9,A10,A17,A26,AFF_1:38;
end;
end;
AP is satisfying_DES2_2 implies AP is satisfying_DES2
proof
assume
A74: AP is satisfying_DES2_2;
thus AP is satisfying_DES2
proof
let A,P,C,a,a9,b,b9,c,c9,p,q;
assume that
A75: A is being_line and
P is being_line and
A76: C is being_line and
A77: A<>P and
A78: A<>C and
A79: P<>C and
A80: a in A & a9 in A and
A81: b in P and
A82: b9 in P and
A83: c in C and
A84: c9 in C and
A85: A // P and
A86: A // C and
A87: not LIN b,a,c and
A88: not LIN b9,a9,c9 and
A89: p<>q and
A90: a<>a9 and
A91: LIN b,a,p and
A92: LIN b9,a9,p and
A93: LIN b,c,q and
A94: LIN b9,c9,q and
A95: a,c // a9,c9;
A96: LIN p,a,b by A91,AFF_1:6;
set A9=Line(a,c), P9=Line(p,q), C9=Line(a9,c9);
A97: q in P9 by A89,AFF_1:24;
A98: a<>p
proof
assume a=p;
then LIN a,a9,b9 by A92,AFF_1:6;
then b9 in A by A75,A80,A90,AFF_1:25;
hence contradiction by A77,A82,A85,AFF_1:45;
end;
A99: not LIN p,a,a9
proof
A100: LIN p,a,a by AFF_1:7;
assume LIN p,a,a9;
then b in A by A75,A80,A90,A98,A96,A100,AFF_1:8,25;
hence contradiction by A77,A81,A85,AFF_1:45;
end;
A101: LIN q,c9,b9 & LIN p,a9,b9 by A92,A94,AFF_1:6;
A102: a<>c by A87,AFF_1:7;
then
A103: A9 is being_line by AFF_1:24;
A104: C // P by A85,A86,AFF_1:44;
then
A105: c,c9 // b,b9 by A81,A82,A83,A84,AFF_1:39;
A106: c <>c9
proof
assume c =c9;
then c,a // c,a9 by A95,AFF_1:4;
then LIN c,a,a9 by AFF_1:def 1;
then LIN a,a9,c by AFF_1:6;
then c in A by A75,A80,A90,AFF_1:25;
hence contradiction by A78,A83,A86,AFF_1:45;
end;
A107: b<>b9
proof
A108: LIN b,p,a & LIN b,p,b by A91,AFF_1:6,7;
assume
A109: b=b9;
then LIN b,p,a9 by A92,AFF_1:6;
then
A110: b=p or b in A by A75,A80,A90,A108,AFF_1:8,25;
A111: LIN b,q,c & LIN b,q,b by A93,AFF_1:6,7;
LIN b,q,c9 by A94,A109,AFF_1:6;
then b=q or b in C by A76,A83,A84,A106,A111,AFF_1:8,25;
hence contradiction by A77,A79,A81,A85,A89,A104,A110,AFF_1:45;
end;
A112: a in A9 & c in A9 by A102,AFF_1:24;
A113: P9 is being_line & c,c9 // a,a9 by A80,A83,A84,A86,A89,AFF_1:24,39;
A114: p in P9 by A89,AFF_1:24;
A115: a9<>c9 by A88,AFF_1:7;
then
A116: a9 in C9 by AFF_1:24;
A117: A9<>C9
proof
assume A9=C9;
then LIN a,a9,c by A103,A112,A116,AFF_1:21;
then c in A by A75,A80,A90,AFF_1:25;
hence contradiction by A78,A83,A86,AFF_1:45;
end;
A118: q<>c
proof
assume q=c;
then LIN c,c9,b9 by A94,AFF_1:6;
then b9 in C by A76,A83,A84,A106,AFF_1:25;
hence contradiction by A79,A82,A104,AFF_1:45;
end;
A119: A9<>P9
proof
assume A9=P9;
then
A120: LIN c,q,a & LIN c,q,c by A103,A112,A97,AFF_1:21;
LIN c,q,b by A93,AFF_1:6;
hence contradiction by A87,A118,A120,AFF_1:8;
end;
A121: LIN q,c,b by A93,AFF_1:6;
A122: not LIN q,c,c9
proof
A123: LIN q,c,c by AFF_1:7;
assume LIN q,c,c9;
then b in C by A76,A83,A84,A106,A118,A121,A123,AFF_1:8,25;
hence contradiction by A79,A81,A104,AFF_1:45;
end;
A124: C9 is being_line & c9 in C9 by A115,AFF_1:24;
then A9 // C9 by A95,A102,A115,A103,A112,A116,AFF_1:38;
then A9 // P9 by A74,A102,A107,A103,A112,A114,A97,A116,A124,A113,A105
,A121,A96,A101,A119,A117,A122,A99;
hence thesis by A112,A114,A97,AFF_1:39;
end;
end;
hence thesis by A1;
end;
theorem
AP is satisfying_DES1_3 implies AP is satisfying_DES2_1
proof
assume
A1: AP is satisfying_DES1_3;
let A,P,C,a,a9,b,b9,c,c9,p,q such that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: A<>P and
A6: A<>C and
A7: P<>C and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p<>q and
A19: LIN b,a,p and
A20: LIN b9,a9,p and
A21: LIN b,c,q and
A22: LIN b9,c9,q and
A23: a,c // p,q;
A24: P // C by A14,A15,AFF_1:44;
set K=Line(p,q), M=Line(a,c), N=Line(a9,c9);
A25: a<>c by A16,AFF_1:7;
then
A26: a in M by AFF_1:24;
A27: c,c9 // a,a9 & LIN q,c,b by A8,A9,A12,A13,A15,A21,AFF_1:6,39;
A28: LIN p,a9,b9 by A20,AFF_1:6;
C // P by A14,A15,AFF_1:44;
then
A29: c,c9 // b,b9 by A10,A11,A12,A13,AFF_1:39;
A30: LIN q,c9,b9 & LIN p,a,b by A19,A22,AFF_1:6;
A31: c in M by A25,AFF_1:24;
assume
A32: not thesis;
A33: c <>q
proof
assume
A34: c =q;
then c,a // c,p by A23,AFF_1:4;
then LIN c,a,p by AFF_1:def 1;
then
A35: LIN p,a,c by AFF_1:6;
LIN p,a,b & LIN p,a,a by A19,AFF_1:6,7;
then p=a by A16,A35,AFF_1:8;
then LIN a,a9,b9 by A20,AFF_1:6;
then
A36: a=a9 or b9 in A by A2,A8,A9,AFF_1:25;
LIN c,c9,b9 by A22,A34,AFF_1:6;
then c =c9 or b9 in C by A4,A12,A13,AFF_1:25;
hence contradiction by A5,A7,A11,A14,A32,A24,A36,AFF_1:2,45;
end;
A37: c <>c9
proof
A38: now
assume
A39: p=b;
LIN b,q,c by A21,AFF_1:6;
then b,q // b,c by AFF_1:def 1;
then a,c // b,c or b=q by A23,A39,AFF_1:5;
then c,a // c,b by A18,A39,AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A16,AFF_1:6;
end;
A40: LIN q,c,b & LIN q,c,c by A21,AFF_1:6,7;
assume
A41: c =c9;
then LIN q,c,b9 by A22,AFF_1:6;
then b=b9 or c in P by A3,A10,A11,A33,A40,AFF_1:8,25;
then
A42: LIN p,b,a9 by A7,A12,A20,A24,AFF_1:6,45;
LIN p,b,a & LIN p,b,b by A19,AFF_1:6,7;
then a=a9 or b in A by A2,A8,A9,A42,A38,AFF_1:8,25;
hence contradiction by A5,A10,A14,A32,A41,AFF_1:2,45;
end;
A43: b<>b9
proof
assume b=b9;
then
A44: LIN q,b,c9 by A22,AFF_1:6;
LIN q,b,c & LIN q,b,b by A21,AFF_1:6,7;
then
A45: q=b or b in C by A4,A12,A13,A37,A44,AFF_1:8,25;
b,a // b,p by A19,AFF_1:def 1;
then a,b // p,b by AFF_1:4;
then a,c // a,b or p=b by A7,A10,A23,A24,A45,AFF_1:5,45;
then LIN a,c,b by A7,A10,A18,A24,A45,AFF_1:45,def 1;
hence contradiction by A16,AFF_1:6;
end;
A46: not LIN q,c,c9
proof
assume
A47: LIN q,c,c9;
LIN q,c,b & LIN q,c,c by A21,AFF_1:6,7;
then b in C by A4,A12,A13,A33,A37,A47,AFF_1:8,25;
hence contradiction by A7,A10,A24,AFF_1:45;
end;
A48: a9<>c9 by A17,AFF_1:7;
then
A49: N is being_line by AFF_1:24;
A50: p<>a
proof
assume p=a;
then LIN a,c,q by A23,AFF_1:def 1;
then
A51: LIN c,q,a by AFF_1:6;
LIN c,q,b & LIN c,q,c by A21,AFF_1:6,7;
hence contradiction by A16,A33,A51,AFF_1:8;
end;
A52: not LIN p,a,a9
proof
assume
A53: LIN p,a,a9;
LIN p,a,b & LIN p,a,a by A19,AFF_1:6,7;
then a=a9 or b in A by A2,A8,A9,A50,A53,AFF_1:8,25;
then
A54: LIN p,a,b9 by A5,A10,A14,A20,AFF_1:6,45;
LIN p,a,b & LIN p,a,a by A19,AFF_1:6,7;
then a in P by A3,A10,A11,A43,A50,A54,AFF_1:8,25;
hence contradiction by A5,A8,A14,AFF_1:45;
end;
A55: M is being_line by A25,AFF_1:24;
A56: K is being_line & q in K by A18,AFF_1:24;
A57: now
assume M=K;
then
A58: LIN q,c,a & LIN q,c,c by A56,A26,A31,AFF_1:21;
LIN q,c,b by A21,AFF_1:6;
hence contradiction by A16,A33,A58,AFF_1:8;
end;
A59: c9 in N by A48,AFF_1:24;
A60: a9 in N by A48,AFF_1:24;
then consider x such that
A61: x in M and
A62: x in N by A32,A55,A49,A26,A31,A59,AFF_1:39,58;
A63: now
assume x=c;
then N=C by A4,A12,A13,A37,A49,A59,A62,AFF_1:18;
hence contradiction by A6,A9,A15,A60,AFF_1:45;
end;
A64: p in K by A18,AFF_1:24;
then
A65: M // K by A18,A23,A25,A55,A56,A26,A31,AFF_1:38;
A66: now
assume x=c9;
then M=C by A4,A12,A13,A37,A55,A31,A61,AFF_1:18;
hence contradiction by A6,A8,A15,A26,AFF_1:45;
end;
M<>N by A32,A55,A26,A31,A60,A59,AFF_1:51;
then x in K by A1,A18,A25,A55,A49,A64,A56,A26,A31,A60,A59,A61,A62,A29,A27,A30
,A28,A43,A63,A66,A46,A52;
hence contradiction by A65,A61,A57,AFF_1:45;
end;