let AP be AffinPlane; :: thesis: ( AP is Pappian implies AP is Desarguesian )

assume A1: AP is Pappian ; :: thesis: AP is Desarguesian

then AP is satisfying_pap by Th9;

then A2: AP is satisfying_PPAP by A1, Th10;

let A be Subset of AP; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let P, C be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A3: o in A and

A4: o in P and

A5: o in C and

A6: o <> a and

A7: o <> b and

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 ; :: thesis: b,c // b9,c9

assume A21: not b,c // b9,c9 ; :: thesis: contradiction

then A22: b <> c by AFF_1:3;

A23: a <> c by A3, A5, A6, A8, A12, A14, A16, A18, AFF_1:18;

A24: not b in C

A27: a <> a9

set N = Line (a9,b9);

set D = Line (a9,c9);

A30: a9 <> b9

A34: a9 <> c9

A76: b9 <> c9 by A21, AFF_1:3;

then A77: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:24;

Line (b9,c9) is being_line by A76, AFF_1:24;

then consider K being Subset of AP such that

A78: o in K and

A79: Line (b9,c9) // K by AFF_1:49;

A80: K is being_line by A79, AFF_1:36;

A81: a9 in Line (a9,b9) by A30, AFF_1:24;

not Line (a9,b9) // K

A82: p in Line (a9,b9) and

A83: p in K by A33, A80, AFF_1:58;

A84: o <> a9

then consider T being Subset of AP such that

A88: p in T and

A89: Line (a9,c9) // T by AFF_1:49;

A90: T is being_line by A89, AFF_1:36;

A91: ( a9 in Line (a9,c9) & c9 in Line (a9,c9) ) by A34, AFF_1:24;

not C // T

A92: q in C and

A93: q in T by A16, A90, AFF_1:58;

A94: b9,c9 // p,o by A77, A78, A79, A83, AFF_1:39;

A95: o <> b9

A98: p <> a

A100: p,q // a9,c9 by A91, A88, A89, A93, AFF_1:39;

then A101: b9,q // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94;

A102: ( a in Line (a,p) & p in Line (a,p) ) by A98, AFF_1:24;

not b9,c9 // A by A14, A21, A40, AFF_1:31;

then A103: K <> A by A77, A79, AFF_1:40;

not b9,q // Line (a,p)

A105: r in Line (a,p) and

A106: LIN b9,q,r by A99, AFF_1:59;

then b9,a9 // b9,p by AFF_1:def 1;

then p,b9 // a9,b9 by AFF_1:4;

then A109: p,b9 // a,b by A19, A30, AFF_1:5;

LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;

then o,a // o,a9 by AFF_1:def 1;

then A110: a,o // a9,o by AFF_1:4;

LIN q,r,b9 by A106, AFF_1:6;

then q,r // q,b9 by AFF_1:def 1;

then r,q // b9,q by AFF_1:4;

then r,q // a9,o by A101, A97, AFF_1:5;

then A111: a,o // r,q by A84, A110, AFF_1:5;

LIN r,b9,q by A106, AFF_1:6;

then r,b9 // r,q by AFF_1:def 1;

then a,o // r,b9 by A111, A107, AFF_1:4, AFF_1:5;

then A112: p,o // r,b by A2, A4, A10, A11, A15, A99, A102, A105, A109;

p,q // a,c by A20, A34, A100, AFF_1:5;

then A113: p,o // r,c by A2, A5, A12, A16, A92, A99, A102, A105, A111;

then r,c // r,b by A86, A112, AFF_1:5;

then LIN r,c,b by AFF_1:def 1;

then LIN c,b,r by AFF_1:6;

then c,b // c,r by AFF_1:def 1;

then A114: b,c // r,c by AFF_1:4;

b9,c9 // r,c by A86, A94, A113, AFF_1:5;

then r = c by A21, A114, AFF_1:5;

then b,c // p,o by A112, AFF_1:4;

hence contradiction by A21, A86, A94, AFF_1:5; :: thesis: verum

assume A1: AP is Pappian ; :: thesis: AP is Desarguesian

then AP is satisfying_pap by Th9;

then A2: AP is satisfying_PPAP by A1, Th10;

let A be Subset of AP; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let P, C be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A3: o in A and

A4: o in P and

A5: o in C and

A6: o <> a and

A7: o <> b and

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 ; :: thesis: b,c // b9,c9

assume A21: not b,c // b9,c9 ; :: thesis: contradiction

then A22: b <> c by AFF_1:3;

A23: a <> c by A3, A5, A6, A8, A12, A14, A16, A18, AFF_1:18;

A24: not b in C

proof

A26:
a <> b
by A3, A4, A6, A8, A10, A14, A15, A17, AFF_1:18;
assume A25:
b in C
; :: thesis: contradiction

then b9 in C by A4, A5, A7, A10, A11, A15, A16, AFF_1:18;

hence contradiction by A12, A13, A16, A21, A25, AFF_1:51; :: thesis: verum

end;then b9 in C by A4, A5, A7, A10, A11, A15, A16, AFF_1:18;

hence contradiction by A12, A13, A16, A21, A25, AFF_1:51; :: thesis: verum

A27: a <> a9

proof

set M = Line (b9,c9);
assume A28:
a = a9
; :: thesis: contradiction

then LIN a,c,c9 by A20, AFF_1:def 1;

then LIN c,c9,a by AFF_1:6;

then A29: ( c = c9 or a in C ) by A12, A13, A16, AFF_1:25;

LIN a,b,b9 by A19, A28, AFF_1:def 1;

then LIN b,b9,a by AFF_1:6;

then ( b = b9 or a in P ) by A10, A11, A15, AFF_1:25;

hence contradiction by A3, A4, A5, A6, A8, A14, A15, A16, A17, A18, A21, A29, AFF_1:2, AFF_1:18; :: thesis: verum

end;then LIN a,c,c9 by A20, AFF_1:def 1;

then LIN c,c9,a by AFF_1:6;

then A29: ( c = c9 or a in C ) by A12, A13, A16, AFF_1:25;

LIN a,b,b9 by A19, A28, AFF_1:def 1;

then LIN b,b9,a by AFF_1:6;

then ( b = b9 or a in P ) by A10, A11, A15, AFF_1:25;

hence contradiction by A3, A4, A5, A6, A8, A14, A15, A16, A17, A18, A21, A29, AFF_1:2, AFF_1:18; :: thesis: verum

set N = Line (a9,b9);

set D = Line (a9,c9);

A30: a9 <> b9

proof

then A33:
Line (a9,b9) is being_line
by AFF_1:24;
A31:
a9,c9 // c,a
by A20, AFF_1:4;

assume A32: a9 = b9 ; :: thesis: contradiction

then a9 in C by A3, A4, A5, A9, A11, A14, A15, A17, AFF_1:18;

then ( a in C or a9 = c9 ) by A12, A13, A16, A31, AFF_1:48;

hence contradiction by A3, A5, A6, A8, A14, A16, A18, A21, A32, AFF_1:3, AFF_1:18; :: thesis: verum

end;assume A32: a9 = b9 ; :: thesis: contradiction

then a9 in C by A3, A4, A5, A9, A11, A14, A15, A17, AFF_1:18;

then ( a in C or a9 = c9 ) by A12, A13, A16, A31, AFF_1:48;

hence contradiction by A3, A5, A6, A8, A14, A16, A18, A21, A32, AFF_1:3, AFF_1:18; :: thesis: verum

A34: a9 <> c9

proof

A36:
not LIN a9,b9,c9
assume
a9 = c9
; :: thesis: contradiction

then A35: a9 in P by A3, A4, A5, A9, A13, A14, A16, A18, AFF_1:18;

a9,b9 // b,a by A19, AFF_1:4;

then a in P by A10, A11, A15, A30, A35, AFF_1:48;

hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; :: thesis: verum

end;then A35: a9 in P by A3, A4, A5, A9, A13, A14, A16, A18, AFF_1:18;

a9,b9 // b,a by A19, AFF_1:4;

then a in P by A10, A11, A15, A30, A35, AFF_1:48;

hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; :: thesis: verum

proof

A39:
not LIN a,b,c
assume A37:
LIN a9,b9,c9
; :: thesis: contradiction

then a9,b9 // a9,c9 by AFF_1:def 1;

then a9,b9 // a,c by A20, A34, AFF_1:5;

then a,b // a,c by A19, A30, AFF_1:5;

then LIN a,b,c by AFF_1:def 1;

then LIN b,c,a by AFF_1:6;

then b,c // b,a by AFF_1:def 1;

then b,c // a,b by AFF_1:4;

then A38: b,c // a9,b9 by A19, A26, AFF_1:5;

LIN b9,c9,a9 by A37, AFF_1:6;

then b9,c9 // b9,a9 by AFF_1:def 1;

then b9,c9 // a9,b9 by AFF_1:4;

hence contradiction by A21, A30, A38, AFF_1:5; :: thesis: verum

end;then a9,b9 // a9,c9 by AFF_1:def 1;

then a9,b9 // a,c by A20, A34, AFF_1:5;

then a,b // a,c by A19, A30, AFF_1:5;

then LIN a,b,c by AFF_1:def 1;

then LIN b,c,a by AFF_1:6;

then b,c // b,a by AFF_1:def 1;

then b,c // a,b by AFF_1:4;

then A38: b,c // a9,b9 by A19, A26, AFF_1:5;

LIN b9,c9,a9 by A37, AFF_1:6;

then b9,c9 // b9,a9 by AFF_1:def 1;

then b9,c9 // a9,b9 by AFF_1:4;

hence contradiction by A21, A30, A38, AFF_1:5; :: thesis: verum

proof

assume
LIN a,b,c
; :: thesis: contradiction

then a,b // a,c by AFF_1:def 1;

then a,b // a9,c9 by A20, A23, AFF_1:5;

then a9,b9 // a9,c9 by A19, A26, AFF_1:5;

hence contradiction by A36, AFF_1:def 1; :: thesis: verum

end;then a,b // a,c by AFF_1:def 1;

then a,b // a9,c9 by A20, A23, AFF_1:5;

then a9,b9 // a9,c9 by A19, A26, AFF_1:5;

hence contradiction by A36, AFF_1:def 1; :: thesis: verum

A40: now :: thesis: b,c // A

A75:
b9 in Line (a9,b9)
by A30, AFF_1:24;
LIN o,a,a9
by A3, A8, A9, A14, AFF_1:21;

then o,a // o,a9 by AFF_1:def 1;

then A41: a9,o // a,o by AFF_1:4;

set M = Line (b,c);

set N = Line (a,b);

set D = Line (a,c);

A42: Line (a,b) is being_line by A26, AFF_1:24;

Line (b,c) is being_line by A22, AFF_1:24;

then consider K being Subset of AP such that

A43: o in K and

A44: Line (b,c) // K by AFF_1:49;

A45: K is being_line by A44, AFF_1:36;

A46: a in Line (a,b) by A26, AFF_1:24;

A47: b in Line (a,b) by A26, AFF_1:24;

A48: ( b in Line (b,c) & c in Line (b,c) ) by A22, AFF_1:24;

not Line (a,b) // K

A49: p in Line (a,b) and

A50: p in K by A42, A45, AFF_1:58;

A51: b,c // p,o by A48, A43, A44, A50, AFF_1:39;

A52: o <> p

A53: p <> a9

Line (a,c) is being_line by A23, AFF_1:24;

then consider T being Subset of AP such that

A55: p in T and

A56: Line (a,c) // T by AFF_1:49;

A57: ( a in Line (a,c) & c in Line (a,c) ) by A23, AFF_1:24;

A58: not C // T

then consider q being Element of AP such that

A59: q in C and

A60: q in T by A16, A58, AFF_1:58;

A61: p,q // a,c by A57, A55, A56, A60, AFF_1:39;

then A62: b,q // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51;

A63: ( a9 in Line (a9,p) & p in Line (a9,p) ) by A53, AFF_1:24;

assume not b,c // A ; :: thesis: contradiction

then A64: K <> A by A48, A44, AFF_1:40;

not b,q // Line (a9,p)

A66: r in Line (a9,p) and

A67: LIN b,q,r by A54, AFF_1:59;

then q,r // q,b by AFF_1:def 1;

then r,q // b,q by AFF_1:4;

then r,q // a,o by A24, A59, A62, AFF_1:5;

then A70: a9,o // r,q by A6, A41, AFF_1:5;

LIN b,a,p by A42, A46, A47, A49, AFF_1:21;

then b,a // b,p by AFF_1:def 1;

then a,b // p,b by AFF_1:4;

then A71: p,b // a9,b9 by A19, A26, AFF_1:5;

LIN r,b,q by A67, AFF_1:6;

then r,b // r,q by AFF_1:def 1;

then a9,o // r,b by A70, A68, AFF_1:4, AFF_1:5;

then A72: p,o // r,b9 by A2, A4, A10, A11, A15, A54, A63, A66, A71;

p,q // a9,c9 by A20, A23, A61, AFF_1:5;

then A73: p,o // r,c9 by A2, A5, A13, A16, A59, A54, A63, A66, A70;

then r,c9 // r,b9 by A52, A72, AFF_1:5;

then LIN r,c9,b9 by AFF_1:def 1;

then LIN c9,b9,r by AFF_1:6;

then c9,b9 // c9,r by AFF_1:def 1;

then A74: r,c9 // b9,c9 by AFF_1:4;

b,c // r,c9 by A52, A51, A73, AFF_1:5;

then r = c9 by A21, A74, AFF_1:5;

then p,o // b9,c9 by A72, AFF_1:4;

hence contradiction by A21, A52, A51, AFF_1:5; :: thesis: verum

end;then o,a // o,a9 by AFF_1:def 1;

then A41: a9,o // a,o by AFF_1:4;

set M = Line (b,c);

set N = Line (a,b);

set D = Line (a,c);

A42: Line (a,b) is being_line by A26, AFF_1:24;

Line (b,c) is being_line by A22, AFF_1:24;

then consider K being Subset of AP such that

A43: o in K and

A44: Line (b,c) // K by AFF_1:49;

A45: K is being_line by A44, AFF_1:36;

A46: a in Line (a,b) by A26, AFF_1:24;

A47: b in Line (a,b) by A26, AFF_1:24;

A48: ( b in Line (b,c) & c in Line (b,c) ) by A22, AFF_1:24;

not Line (a,b) // K

proof

then consider p being Element of AP such that
assume
Line (a,b) // K
; :: thesis: contradiction

then Line (a,b) // Line (b,c) by A44, AFF_1:44;

then c in Line (a,b) by A48, A47, AFF_1:45;

hence contradiction by A39, A42, A46, A47, AFF_1:21; :: thesis: verum

end;then Line (a,b) // Line (b,c) by A44, AFF_1:44;

then c in Line (a,b) by A48, A47, AFF_1:45;

hence contradiction by A39, A42, A46, A47, AFF_1:21; :: thesis: verum

A49: p in Line (a,b) and

A50: p in K by A42, A45, AFF_1:58;

A51: b,c // p,o by A48, A43, A44, A50, AFF_1:39;

A52: o <> p

proof

set R = Line (a9,p);
assume
o = p
; :: thesis: contradiction

then LIN o,a,b by A42, A46, A47, A49, AFF_1:21;

then b in A by A3, A6, A8, A14, AFF_1:25;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

end;then LIN o,a,b by A42, A46, A47, A49, AFF_1:21;

then b in A by A3, A6, A8, A14, AFF_1:25;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

A53: p <> a9

proof

then A54:
Line (a9,p) is being_line
by AFF_1:24;
assume
p = a9
; :: thesis: contradiction

then b in A by A8, A9, A14, A27, A42, A46, A47, A49, AFF_1:18;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

end;then b in A by A8, A9, A14, A27, A42, A46, A47, A49, AFF_1:18;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

Line (a,c) is being_line by A23, AFF_1:24;

then consider T being Subset of AP such that

A55: p in T and

A56: Line (a,c) // T by AFF_1:49;

A57: ( a in Line (a,c) & c in Line (a,c) ) by A23, AFF_1:24;

A58: not C // T

proof

T is being_line
by A56, AFF_1:36;
assume
C // T
; :: thesis: contradiction

then C // Line (a,c) by A56, AFF_1:44;

then a in C by A12, A57, AFF_1:45;

hence contradiction by A3, A5, A6, A8, A14, A16, A18, AFF_1:18; :: thesis: verum

end;then C // Line (a,c) by A56, AFF_1:44;

then a in C by A12, A57, AFF_1:45;

hence contradiction by A3, A5, A6, A8, A14, A16, A18, AFF_1:18; :: thesis: verum

then consider q being Element of AP such that

A59: q in C and

A60: q in T by A16, A58, AFF_1:58;

A61: p,q // a,c by A57, A55, A56, A60, AFF_1:39;

then A62: b,q // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51;

A63: ( a9 in Line (a9,p) & p in Line (a9,p) ) by A53, AFF_1:24;

assume not b,c // A ; :: thesis: contradiction

then A64: K <> A by A48, A44, AFF_1:40;

not b,q // Line (a9,p)

proof

then consider r being Element of AP such that
assume
b,q // Line (a9,p)
; :: thesis: contradiction

then A65: a,o // Line (a9,p) by A24, A59, A62, AFF_1:32;

a,o // A by A3, A8, A14, AFF_1:40, AFF_1:41;

then p in A by A6, A9, A63, A65, AFF_1:45, AFF_1:53;

hence contradiction by A3, A14, A43, A45, A50, A52, A64, AFF_1:18; :: thesis: verum

end;then A65: a,o // Line (a9,p) by A24, A59, A62, AFF_1:32;

a,o // A by A3, A8, A14, AFF_1:40, AFF_1:41;

then p in A by A6, A9, A63, A65, AFF_1:45, AFF_1:53;

hence contradiction by A3, A14, A43, A45, A50, A52, A64, AFF_1:18; :: thesis: verum

A66: r in Line (a9,p) and

A67: LIN b,q,r by A54, AFF_1:59;

A68: now :: thesis: ( r = q implies r,b // o,a9 )

LIN q,r,b
by A67, AFF_1:6;assume
r = q
; :: thesis: r,b // o,a9

then b,r // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, A61;

then A69: r,b // o,a by AFF_1:4;

LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;

then o,a // o,a9 by AFF_1:def 1;

hence r,b // o,a9 by A6, A69, AFF_1:5; :: thesis: verum

end;then b,r // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, A61;

then A69: r,b // o,a by AFF_1:4;

LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;

then o,a // o,a9 by AFF_1:def 1;

hence r,b // o,a9 by A6, A69, AFF_1:5; :: thesis: verum

then q,r // q,b by AFF_1:def 1;

then r,q // b,q by AFF_1:4;

then r,q // a,o by A24, A59, A62, AFF_1:5;

then A70: a9,o // r,q by A6, A41, AFF_1:5;

LIN b,a,p by A42, A46, A47, A49, AFF_1:21;

then b,a // b,p by AFF_1:def 1;

then a,b // p,b by AFF_1:4;

then A71: p,b // a9,b9 by A19, A26, AFF_1:5;

LIN r,b,q by A67, AFF_1:6;

then r,b // r,q by AFF_1:def 1;

then a9,o // r,b by A70, A68, AFF_1:4, AFF_1:5;

then A72: p,o // r,b9 by A2, A4, A10, A11, A15, A54, A63, A66, A71;

p,q // a9,c9 by A20, A23, A61, AFF_1:5;

then A73: p,o // r,c9 by A2, A5, A13, A16, A59, A54, A63, A66, A70;

then r,c9 // r,b9 by A52, A72, AFF_1:5;

then LIN r,c9,b9 by AFF_1:def 1;

then LIN c9,b9,r by AFF_1:6;

then c9,b9 // c9,r by AFF_1:def 1;

then A74: r,c9 // b9,c9 by AFF_1:4;

b,c // r,c9 by A52, A51, A73, AFF_1:5;

then r = c9 by A21, A74, AFF_1:5;

then p,o // b9,c9 by A72, AFF_1:4;

hence contradiction by A21, A52, A51, AFF_1:5; :: thesis: verum

A76: b9 <> c9 by A21, AFF_1:3;

then A77: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:24;

Line (b9,c9) is being_line by A76, AFF_1:24;

then consider K being Subset of AP such that

A78: o in K and

A79: Line (b9,c9) // K by AFF_1:49;

A80: K is being_line by A79, AFF_1:36;

A81: a9 in Line (a9,b9) by A30, AFF_1:24;

not Line (a9,b9) // K

proof

then consider p being Element of AP such that
assume
Line (a9,b9) // K
; :: thesis: contradiction

then Line (a9,b9) // Line (b9,c9) by A79, AFF_1:44;

then c9 in Line (a9,b9) by A77, A75, AFF_1:45;

hence contradiction by A36, A33, A81, A75, AFF_1:21; :: thesis: verum

end;then Line (a9,b9) // Line (b9,c9) by A79, AFF_1:44;

then c9 in Line (a9,b9) by A77, A75, AFF_1:45;

hence contradiction by A36, A33, A81, A75, AFF_1:21; :: thesis: verum

A82: p in Line (a9,b9) and

A83: p in K by A33, A80, AFF_1:58;

A84: o <> a9

proof

A86:
o <> p
assume A85:
o = a9
; :: thesis: contradiction

a9,b9 // b,a by A19, AFF_1:4;

then a in P by A4, A10, A11, A15, A30, A85, AFF_1:48;

hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; :: thesis: verum

end;a9,b9 // b,a by A19, AFF_1:4;

then a in P by A4, A10, A11, A15, A30, A85, AFF_1:48;

hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; :: thesis: verum

proof

Line (a9,c9) is being_line
by A34, AFF_1:24;
assume
o = p
; :: thesis: contradiction

then LIN o,a9,b9 by A33, A81, A75, A82, AFF_1:21;

then A87: b9 in A by A3, A9, A14, A84, AFF_1:25;

a9,b9 // a,b by A19, AFF_1:4;

then b in A by A8, A9, A14, A30, A87, AFF_1:48;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

end;then LIN o,a9,b9 by A33, A81, A75, A82, AFF_1:21;

then A87: b9 in A by A3, A9, A14, A84, AFF_1:25;

a9,b9 // a,b by A19, AFF_1:4;

then b in A by A8, A9, A14, A30, A87, AFF_1:48;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

then consider T being Subset of AP such that

A88: p in T and

A89: Line (a9,c9) // T by AFF_1:49;

A90: T is being_line by A89, AFF_1:36;

A91: ( a9 in Line (a9,c9) & c9 in Line (a9,c9) ) by A34, AFF_1:24;

not C // T

proof

then consider q being Element of AP such that
assume
C // T
; :: thesis: contradiction

then C // Line (a9,c9) by A89, AFF_1:44;

then a9 in C by A13, A91, AFF_1:45;

hence contradiction by A3, A5, A9, A14, A16, A18, A84, AFF_1:18; :: thesis: verum

end;then C // Line (a9,c9) by A89, AFF_1:44;

then a9 in C by A13, A91, AFF_1:45;

hence contradiction by A3, A5, A9, A14, A16, A18, A84, AFF_1:18; :: thesis: verum

A92: q in C and

A93: q in T by A16, A90, AFF_1:58;

A94: b9,c9 // p,o by A77, A78, A79, A83, AFF_1:39;

A95: o <> b9

proof

A97:
b9 <> q
assume A96:
o = b9
; :: thesis: contradiction

b9,a9 // a,b by A19, AFF_1:4;

then b in A by A3, A8, A9, A14, A30, A96, AFF_1:48;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

end;b9,a9 // a,b by A19, AFF_1:4;

then b in A by A3, A8, A9, A14, A30, A96, AFF_1:48;

hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum

proof

set R = Line (a,p);
assume
b9 = q
; :: thesis: contradiction

then P = C by A4, A5, A11, A15, A16, A95, A92, AFF_1:18;

hence contradiction by A10, A11, A12, A13, A15, A21, AFF_1:51; :: thesis: verum

end;then P = C by A4, A5, A11, A15, A16, A95, A92, AFF_1:18;

hence contradiction by A10, A11, A12, A13, A15, A21, AFF_1:51; :: thesis: verum

A98: p <> a

proof

then A99:
Line (a,p) is being_line
by AFF_1:24;
assume
p = a
; :: thesis: contradiction

then b9 in A by A8, A9, A14, A27, A33, A81, A75, A82, AFF_1:18;

hence contradiction by A3, A4, A11, A14, A15, A17, A95, AFF_1:18; :: thesis: verum

end;then b9 in A by A8, A9, A14, A27, A33, A81, A75, A82, AFF_1:18;

hence contradiction by A3, A4, A11, A14, A15, A17, A95, AFF_1:18; :: thesis: verum

A100: p,q // a9,c9 by A91, A88, A89, A93, AFF_1:39;

then A101: b9,q // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94;

A102: ( a in Line (a,p) & p in Line (a,p) ) by A98, AFF_1:24;

not b9,c9 // A by A14, A21, A40, AFF_1:31;

then A103: K <> A by A77, A79, AFF_1:40;

not b9,q // Line (a,p)

proof

then consider r being Element of AP such that
assume
b9,q // Line (a,p)
; :: thesis: contradiction

then A104: a9,o // Line (a,p) by A101, A97, AFF_1:32;

a9,o // A by A3, A9, A14, AFF_1:40, AFF_1:41;

then p in A by A8, A84, A102, A104, AFF_1:45, AFF_1:53;

hence contradiction by A3, A14, A78, A80, A83, A86, A103, AFF_1:18; :: thesis: verum

end;then A104: a9,o // Line (a,p) by A101, A97, AFF_1:32;

a9,o // A by A3, A9, A14, AFF_1:40, AFF_1:41;

then p in A by A8, A84, A102, A104, AFF_1:45, AFF_1:53;

hence contradiction by A3, A14, A78, A80, A83, A86, A103, AFF_1:18; :: thesis: verum

A105: r in Line (a,p) and

A106: LIN b9,q,r by A99, AFF_1:59;

A107: now :: thesis: ( r = q implies r,b9 // o,a )

LIN b9,a9,p
by A33, A81, A75, A82, AFF_1:21;assume
r = q
; :: thesis: r,b9 // o,a

then b9,r // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, A100;

then A108: r,b9 // o,a9 by AFF_1:4;

LIN o,a9,a by A3, A8, A9, A14, AFF_1:21;

then o,a9 // o,a by AFF_1:def 1;

hence r,b9 // o,a by A84, A108, AFF_1:5; :: thesis: verum

end;then b9,r // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, A100;

then A108: r,b9 // o,a9 by AFF_1:4;

LIN o,a9,a by A3, A8, A9, A14, AFF_1:21;

then o,a9 // o,a by AFF_1:def 1;

hence r,b9 // o,a by A84, A108, AFF_1:5; :: thesis: verum

then b9,a9 // b9,p by AFF_1:def 1;

then p,b9 // a9,b9 by AFF_1:4;

then A109: p,b9 // a,b by A19, A30, AFF_1:5;

LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;

then o,a // o,a9 by AFF_1:def 1;

then A110: a,o // a9,o by AFF_1:4;

LIN q,r,b9 by A106, AFF_1:6;

then q,r // q,b9 by AFF_1:def 1;

then r,q // b9,q by AFF_1:4;

then r,q // a9,o by A101, A97, AFF_1:5;

then A111: a,o // r,q by A84, A110, AFF_1:5;

LIN r,b9,q by A106, AFF_1:6;

then r,b9 // r,q by AFF_1:def 1;

then a,o // r,b9 by A111, A107, AFF_1:4, AFF_1:5;

then A112: p,o // r,b by A2, A4, A10, A11, A15, A99, A102, A105, A109;

p,q // a,c by A20, A34, A100, AFF_1:5;

then A113: p,o // r,c by A2, A5, A12, A16, A92, A99, A102, A105, A111;

then r,c // r,b by A86, A112, AFF_1:5;

then LIN r,c,b by AFF_1:def 1;

then LIN c,b,r by AFF_1:6;

then c,b // c,r by AFF_1:def 1;

then A114: b,c // r,c by AFF_1:4;

b9,c9 // r,c by A86, A94, A113, AFF_1:5;

then r = c by A21, A114, AFF_1:5;

then b,c // p,o by A112, AFF_1:4;

hence contradiction by A21, A86, A94, AFF_1:5; :: thesis: verum