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 Th23;
then A2: AP is satisfying_PPAP by A1, Th24;
thus AP is Desarguesian :: thesis: verum

proof

let A be Subset of ; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of
for o, a, b, c, a', b', c' being Element of st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let P, C be Subset of ; :: thesis: for o, a, b, c, a', b', c' being Element of st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let o, a, b, c, a', b', c' be Element of ; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
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: 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 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 // a',b' and
A20: a,c // a',c' ; :: thesis: b,c // b',c'
assume A21: not b,c // b',c' ; :: thesis: contradiction
then A22: b <> c by AFF_1:12;
A23: a <> c by A3, A5, A6, A8, A12, A14, A16, A18, AFF_1:30;
A24: not b in C

proof

assume A25: b in C ; :: thesis: contradiction
then b' in C by A4, A5, A7, A10, A11, A15, A16, AFF_1:30;
hence contradiction by A12, A13, A16, A21, A25, AFF_1:65; :: thesis: verum

end;

A26: a <> b by A3, A4, A6, A8, A10, A14, A15, A17, AFF_1:30;
A27: a <> a'

proof

assume A28: a = a' ; :: thesis: contradiction
then LIN a,c,c' by A20, AFF_1:def 1;
then LIN c,c',a by AFF_1:15;
then A29: ( c = c' or a in C ) by A12, A13, A16, AFF_1:39;
LIN a,b,b' by A19, A28, AFF_1:def 1;
then LIN b,b',a by AFF_1:15;
then ( b = b' or a in P ) by A10, A11, A15, AFF_1:39;
hence contradiction by A3, A4, A5, A6, A8, A14, A15, A16, A17, A18, A21, A29, AFF_1:11, AFF_1:30; :: thesis: verum

end;

set M = Line b',c';
set N = Line a',b';
set D = Line a',c';
A30: a' <> b'

proof

A31: a',c' // c,a by A20, AFF_1:13;
assume A32: a' = b' ; :: thesis: contradiction
then a' in C by A3, A4, A5, A9, A11, A14, A15, A17, AFF_1:30;
then ( a in C or a' = c' ) by A12, A13, A16, A31, AFF_1:62;
hence contradiction by A3, A5, A6, A8, A14, A16, A18, A21, A32, AFF_1:12, AFF_1:30; :: thesis: verum

end;

then A33: Line a',b' is being_line by AFF_1:38;
A34: a' <> c'

proof

assume a' = c' ; :: thesis: contradiction
then A35: a' in P by A3, A4, A5, A9, A13, A14, A16, A18, AFF_1:30;
a',b' // b,a by A19, AFF_1:13;
then a in P by A10, A11, A15, A30, A35, AFF_1:62;
hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

A36: not LIN a',b',c'

proof

assume A37: LIN a',b',c' ; :: thesis: contradiction
then a',b' // a',c' by AFF_1:def 1;
then a',b' // a,c by A20, A34, AFF_1:14;
then a,b // a,c by A19, A30, AFF_1:14;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:15;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:13;
then A38: b,c // a',b' by A19, A26, AFF_1:14;
LIN b',c',a' by A37, AFF_1:15;
then b',c' // b',a' by AFF_1:def 1;
then b',c' // a',b' by AFF_1:13;
hence contradiction by A21, A30, A38, AFF_1:14; :: thesis: verum

end;

A39: not LIN a,b,c

proof

assume LIN a,b,c ; :: thesis: contradiction
then a,b // a,c by AFF_1:def 1;
then a,b // a',c' by A20, A23, AFF_1:14;
then a',b' // a',c' by A19, A26, AFF_1:14;
hence contradiction by A36, AFF_1:def 1; :: thesis: verum

end;

A40: now

LIN o,a,a' by A3, A8, A9, A14, AFF_1:33;
then o,a // o,a' by AFF_1:def 1;
then A41: a',o // a,o by AFF_1:13;
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:38;
Line b,c is being_line by A22, AFF_1:38;
then consider K being Subset of such that
A43: o in K and
A44: Line b,c // K by AFF_1:63;
A45: K is being_line by A44, AFF_1:50;
A46: a in Line a,b by A26, AFF_1:38;
A47: b in Line a,b by A26, AFF_1:38;
A48: ( b in Line b,c & c in Line b,c ) by A22, AFF_1:38;
not Line a,b // K

proof

assume Line a,b // K ; :: thesis: contradiction
then Line a,b // Line b,c by A44, AFF_1:58;
then c in Line a,b by A48, A47, AFF_1:59;
hence contradiction by A39, A42, A46, A47, AFF_1:33; :: thesis: verum

end;

then consider p being Element of such that
A49: p in Line a,b and
A50: p in K by A42, A45, AFF_1:72;
A51: b,c // p,o by A48, A43, A44, A50, AFF_1:53;
A52: o <> p

proof

assume o = p ; :: thesis: contradiction
then LIN o,a,b by A42, A46, A47, A49, AFF_1:33;
then b in A by A3, A6, A8, A14, AFF_1:39;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

set R = Line a',p;
A53: p <> a'

proof

assume p = a' ; :: thesis: contradiction
then b in A by A8, A9, A14, A27, A42, A46, A47, A49, AFF_1:30;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

then A54: Line a',p is being_line by AFF_1:38;
Line a,c is being_line by A23, AFF_1:38;
then consider T being Subset of such that
A55: p in T and
A56: Line a,c // T by AFF_1:63;
A57: ( a in Line a,c & c in Line a,c ) by A23, AFF_1:38;
A58: not C // T

proof

assume C // T ; :: thesis: contradiction
then C // Line a,c by A56, AFF_1:58;
then a in C by A12, A57, AFF_1:59;
hence contradiction by A3, A5, A6, A8, A14, A16, A18, AFF_1:30; :: thesis: verum

end;

T is being_line by A56, AFF_1:50;
then consider q being Element of such that
A59: q in C and
A60: q in T by A16, A58, AFF_1:72;
A61: p,q // a,c by A57, A55, A56, A60, AFF_1:53;
then A62: b,q // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, Def1;
A63: ( a' in Line a',p & p in Line a',p ) by A53, AFF_1:38;
assume not b,c // A ; :: thesis: contradiction
then A64: K <> A by A48, A44, AFF_1:54;
not b,q // Line a',p

proof

assume b,q // Line a',p ; :: thesis: contradiction
then A65: a,o // Line a',p by A24, A59, A62, AFF_1:46;
a,o // A by A3, A8, A14, AFF_1:54, AFF_1:55;
then p in A by A6, A9, A63, A65, AFF_1:59, AFF_1:67;
hence contradiction by A3, A14, A43, A45, A50, A52, A64, AFF_1:30; :: thesis: verum

end;

then consider r being Element of such that
A66: r in Line a',p and
A67: LIN b,q,r by A54, AFF_1:73;

A68: now

assume r = q ; :: thesis: r,b // o,a'
then b,r // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, A61, Def1;
then A69: r,b // o,a by AFF_1:13;
LIN o,a,a' by A3, A8, A9, A14, AFF_1:33;
then o,a // o,a' by AFF_1:def 1;
hence r,b // o,a' by A6, A69, AFF_1:14; :: thesis: verum

end;

LIN q,r,b by A67, AFF_1:15;
then q,r // q,b by AFF_1:def 1;
then r,q // b,q by AFF_1:13;
then r,q // a,o by A24, A59, A62, AFF_1:14;
then A70: a',o // r,q by A6, A41, AFF_1:14;
LIN b,a,p by A42, A46, A47, A49, AFF_1:33;
then b,a // b,p by AFF_1:def 1;
then a,b // p,b by AFF_1:13;
then A71: p,b // a',b' by A19, A26, AFF_1:14;
LIN r,b,q by A67, AFF_1:15;
then r,b // r,q by AFF_1:def 1;
then a',o // r,b by A70, A68, AFF_1:13, AFF_1:14;
then A72: p,o // r,b' by A2, A4, A10, A11, A15, A54, A63, A66, A71, Def1;
p,q // a',c' by A20, A23, A61, AFF_1:14;
then A73: p,o // r,c' by A2, A5, A13, A16, A59, A54, A63, A66, A70, Def1;
then r,c' // r,b' by A52, A72, AFF_1:14;
then LIN r,c',b' by AFF_1:def 1;
then LIN c',b',r by AFF_1:15;
then c',b' // c',r by AFF_1:def 1;
then A74: r,c' // b',c' by AFF_1:13;
b,c // r,c' by A52, A51, A73, AFF_1:14;
then r = c' by A21, A74, AFF_1:14;
then p,o // b',c' by A72, AFF_1:13;
hence contradiction by A21, A52, A51, AFF_1:14; :: thesis: verum

end;

A75: b' in Line a',b' by A30, AFF_1:38;
A76: b' <> c' by A21, AFF_1:12;
then A77: ( b' in Line b',c' & c' in Line b',c' ) by AFF_1:38;
Line b',c' is being_line by A76, AFF_1:38;
then consider K being Subset of such that
A78: o in K and
A79: Line b',c' // K by AFF_1:63;
A80: K is being_line by A79, AFF_1:50;
A81: a' in Line a',b' by A30, AFF_1:38;
not Line a',b' // K

proof

assume Line a',b' // K ; :: thesis: contradiction
then Line a',b' // Line b',c' by A79, AFF_1:58;
then c' in Line a',b' by A77, A75, AFF_1:59;
hence contradiction by A36, A33, A81, A75, AFF_1:33; :: thesis: verum

end;

then consider p being Element of such that
A82: p in Line a',b' and
A83: p in K by A33, A80, AFF_1:72;
A84: o <> a'

proof

assume A85: o = a' ; :: thesis: contradiction
a',b' // b,a by A19, AFF_1:13;
then a in P by A4, A10, A11, A15, A30, A85, AFF_1:62;
hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

A86: o <> p

proof

assume o = p ; :: thesis: contradiction
then LIN o,a',b' by A33, A81, A75, A82, AFF_1:33;
then A87: b' in A by A3, A9, A14, A84, AFF_1:39;
a',b' // a,b by A19, AFF_1:13;
then b in A by A8, A9, A14, A30, A87, AFF_1:62;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

Line a',c' is being_line by A34, AFF_1:38;
then consider T being Subset of such that
A88: p in T and
A89: Line a',c' // T by AFF_1:63;
A90: T is being_line by A89, AFF_1:50;
A91: ( a' in Line a',c' & c' in Line a',c' ) by A34, AFF_1:38;
not C // T

proof

assume C // T ; :: thesis: contradiction
then C // Line a',c' by A89, AFF_1:58;
then a' in C by A13, A91, AFF_1:59;
hence contradiction by A3, A5, A9, A14, A16, A18, A84, AFF_1:30; :: thesis: verum

end;

then consider q being Element of such that
A92: q in C and
A93: q in T by A16, A90, AFF_1:72;
A94: b',c' // p,o by A77, A78, A79, A83, AFF_1:53;
A95: o <> b'

proof

assume A96: o = b' ; :: thesis: contradiction
b',a' // a,b by A19, AFF_1:13;
then b in A by A3, A8, A9, A14, A30, A96, AFF_1:62;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

A97: b' <> q

proof

assume b' = q ; :: thesis: contradiction
then P = C by A4, A5, A11, A15, A16, A95, A92, AFF_1:30;
hence contradiction by A10, A11, A12, A13, A15, A21, AFF_1:65; :: thesis: verum

end;

set R = Line a,p;
A98: p <> a

proof

assume p = a ; :: thesis: contradiction
then b' in A by A8, A9, A14, A27, A33, A81, A75, A82, AFF_1:30;
hence contradiction by A3, A4, A11, A14, A15, A17, A95, AFF_1:30; :: thesis: verum

end;

then A99: Line a,p is being_line by AFF_1:38;
A100: p,q // a',c' by A91, A88, A89, A93, AFF_1:53;
then A101: b',q // a',o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, Def1;
A102: ( a in Line a,p & p in Line a,p ) by A98, AFF_1:38;
not b',c' // A by A14, A21, A40, AFF_1:45;
then A103: K <> A by A77, A79, AFF_1:54;
not b',q // Line a,p

proof

assume b',q // Line a,p ; :: thesis: contradiction
then A104: a',o // Line a,p by A101, A97, AFF_1:46;
a',o // A by A3, A9, A14, AFF_1:54, AFF_1:55;
then p in A by A8, A84, A102, A104, AFF_1:59, AFF_1:67;
hence contradiction by A3, A14, A78, A80, A83, A86, A103, AFF_1:30; :: thesis: verum

end;

then consider r being Element of such that
A105: r in Line a,p and
A106: LIN b',q,r by A99, AFF_1:73;

A107: now

assume r = q ; :: thesis: r,b' // o,a
then b',r // a',o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, A100, Def1;
then A108: r,b' // o,a' by AFF_1:13;
LIN o,a',a by A3, A8, A9, A14, AFF_1:33;
then o,a' // o,a by AFF_1:def 1;
hence r,b' // o,a by A84, A108, AFF_1:14; :: thesis: verum

end;

LIN b',a',p by A33, A81, A75, A82, AFF_1:33;
then b',a' // b',p by AFF_1:def 1;
then p,b' // a',b' by AFF_1:13;
then A109: p,b' // a,b by A19, A30, AFF_1:14;
LIN o,a,a' by A3, A8, A9, A14, AFF_1:33;
then o,a // o,a' by AFF_1:def 1;
then A110: a,o // a',o by AFF_1:13;
LIN q,r,b' by A106, AFF_1:15;
then q,r // q,b' by AFF_1:def 1;
then r,q // b',q by AFF_1:13;
then r,q // a',o by A101, A97, AFF_1:14;
then A111: a,o // r,q by A84, A110, AFF_1:14;
LIN r,b',q by A106, AFF_1:15;
then r,b' // r,q by AFF_1:def 1;
then a,o // r,b' by A111, A107, AFF_1:13, AFF_1:14;
then A112: p,o // r,b by A2, A4, A10, A11, A15, A99, A102, A105, A109, Def1;
p,q // a,c by A20, A34, A100, AFF_1:14;
then A113: p,o // r,c by A2, A5, A12, A16, A92, A99, A102, A105, A111, Def1;
then r,c // r,b by A86, A112, AFF_1:14;
then LIN r,c,b by AFF_1:def 1;
then LIN c,b,r by AFF_1:15;
then c,b // c,r by AFF_1:def 1;
then A114: b,c // r,c by AFF_1:13;
b',c' // r,c by A86, A94, A113, AFF_1:14;
then r = c by A21, A114, AFF_1:14;
then b,c // p,o by A112, AFF_1:13;
hence contradiction by A21, A86, A94, AFF_1:14; :: thesis: verum

end;