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 AP; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is 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 AP; :: thesis: for o, a, b, c, a', b', c' being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is 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 AP; :: 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 A3: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'
assume A4: not b,c // b',c' ; :: thesis: contradiction
then A5: ( b <> c & b' <> c' ) by AFF_1:12;
A6: ( a <> b & a <> c ) by A3, AFF_1:30;
A7: a <> a'

proof

assume a = a' ; :: thesis: contradiction
then ( LIN a,b,b' & LIN a,c,c' ) by A3, AFF_1:def 1;
then ( LIN b,b',a & LIN c,c',a ) by AFF_1:15;
then ( ( b = b' or a in P ) & ( c = c' or a in C ) ) by A3, AFF_1:39;
hence contradiction by A3, A4, AFF_1:11, AFF_1:30; :: thesis: verum

end;

A8: a' <> b'

proof

assume A9: a' = b' ; :: thesis: contradiction
then ( a' in C & a',c' // c,a ) by A3, AFF_1:13, AFF_1:30;
then ( a in C or a' = c' ) by A3, AFF_1:62;
hence contradiction by A3, A4, A9, AFF_1:12, AFF_1:30; :: thesis: verum

end;

A10: a' <> c'

proof

assume a' = c' ; :: thesis: contradiction
then ( a' in P & a',b' // b,a ) by A3, AFF_1:13, AFF_1:30;
then ( a' in P & a in P ) by A3, A8, AFF_1:62;
hence contradiction by A3, AFF_1:30; :: thesis: verum

end;

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

proof

assume LIN a',b',c' ; :: thesis: contradiction
then ( a',b' // a',c' & LIN b',c',a' ) by AFF_1:15, AFF_1:def 1;
then A12: ( a',b' // a,c & b',c' // b',a' ) by A3, A10, AFF_1:14, AFF_1:def 1;
then a,b // a,c by A3, A8, AFF_1:14;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:15;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:13;
then ( b,c // a',b' & b',c' // a',b' ) by A3, A6, A12, AFF_1:13, AFF_1:14;
hence contradiction by A4, A8, AFF_1:14; :: thesis: verum

end;

A13: 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 A3, A6, AFF_1:14;
then a',b' // a',c' by A3, A6, AFF_1:14;
hence contradiction by A11, AFF_1:def 1; :: thesis: verum

end;

A14: not b in C

proof

assume b in C ; :: thesis: contradiction
then ( b in C & b' in C ) by A3, AFF_1:30;
hence contradiction by A3, A4, AFF_1:65; :: thesis: verum

end;

A15: o <> a'

proof

assume o = a' ; :: thesis: contradiction
then ( a' in P & a',b' // b,a ) by A3, AFF_1:13;
then ( a in P & a' in P ) by A3, A8, AFF_1:62;
hence contradiction by A3, AFF_1:30; :: thesis: verum

end;

A16: o <> b'

proof

assume o = b' ; :: thesis: contradiction
then ( b' in A & b',a' // a,b ) by A3, AFF_1:13;
then ( b in A & b' in A ) by A3, A8, AFF_1:62;
hence contradiction by A3, AFF_1:30; :: thesis: verum

end;

now

assume A17: not b,c // A ; :: thesis: contradiction
set M = Line b,c;
set N = Line a,b;
set D = Line a,c;
A18: ( Line b,c is being_line & Line a,b is being_line & b in Line b,c & Line a,c is being_line & c in Line b,c & a in Line a,b & b in Line a,b & a in Line a,c & c in Line a,c ) by A5, A6, AFF_1:38;
then consider K being Subset of AP such that
A19: ( o in K & Line b,c // K ) by AFF_1:63;
A20: ( K is being_line & K // Line b,c ) by A19, AFF_1:50;
not Line a,b // K

proof

assume Line a,b // K ; :: thesis: contradiction
then Line a,b // Line b,c by A19, AFF_1:58;
then c in Line a,b by A18, AFF_1:59;
hence contradiction by A13, A18, AFF_1:33; :: thesis: verum

end;

then consider p being Element of AP such that
A21: ( p in Line a,b & p in K ) by A18, A20, AFF_1:72;
consider T being Subset of AP such that
A22: ( p in T & Line a,c // T ) by A18, AFF_1:63;
A23: ( T is being_line & T // Line a,c ) by A22, AFF_1:50;
not C // T

proof

assume C // T ; :: thesis: contradiction
then C // Line a,c by A22, AFF_1:58;
then a in C by A3, A18, AFF_1:59;
hence contradiction by A3, AFF_1:30; :: thesis: verum

end;

then consider q being Element of AP such that
A24: ( q in C & q in T ) by A3, A23, AFF_1:72;
A25: o <> p

proof

assume o = p ; :: thesis: contradiction
then ( LIN o,a,b & LIN o,a,a' & LIN o,a,a ) by A3, A18, A21, AFF_1:33;
then b in A by A3, AFF_1:39;
hence contradiction by A3, AFF_1:30; :: thesis: verum

end;

A26: ( b,c // p,o & p,q // a,c ) by A18, A19, A21, A22, A24, AFF_1:53;
then A27: b,q // a,o by A2, A3, A18, A21, A24, Def1;
A28: p <> a'

proof

assume p = a' ; :: thesis: contradiction
then b in A by A3, A7, A18, A21, AFF_1:30;
hence contradiction by A3, AFF_1:30; :: thesis: verum

end;

A29: K <> A by A17, A18, A19, AFF_1:54;
set R = Line a',p;
A30: ( Line a',p is being_line & a' in Line a',p & p in Line a',p ) by A28, AFF_1:38;
not b,q // Line a',p

proof

assume b,q // Line a',p ; :: thesis: contradiction
then ( a,o // Line a',p & A // A ) by A3, A14, A24, A27, AFF_1:46, AFF_1:55;
then ( a,o // Line a',p & a,o // A ) by A3, AFF_1:54;
then p in A by A3, A30, AFF_1:59, AFF_1:67;
hence contradiction by A3, A19, A20, A21, A25, A29, AFF_1:30; :: thesis: verum

end;

then consider r being Element of AP such that
A31: ( r in Line a',p & LIN b,q,r ) by A30, AFF_1:73;
A32: p,q // a',c' by A3, A6, A26, AFF_1:14;
A33: a',o // r,q

proof

LIN q,r,b by A31, AFF_1:15;
then q,r // q,b by AFF_1:def 1;
then r,q // b,q by AFF_1:13;
then A34: r,q // a,o by A14, A24, A27, AFF_1:14;
LIN o,a,a' by A3, AFF_1:33;
then o,a // o,a' by AFF_1:def 1;
then a',o // a,o by AFF_1:13;
hence a',o // r,q by A3, A34, AFF_1:14; :: thesis: verum

end;

then A35: p,o // r,c' by A2, A3, A24, A30, A31, A32, Def1;
then A36: b,c // r,c' by A25, A26, AFF_1:14;
A37: p,b // a',b'

proof

LIN b,a,p by A18, A21, AFF_1:33;
then b,a // b,p by AFF_1:def 1;
then a,b // p,b by AFF_1:13;
hence p,b // a',b' by A3, A6, AFF_1:14; :: thesis: verum

end;

a',o // r,b

proof

LIN r,b,q by A31, AFF_1:15;
then A38: r,b // r,q by AFF_1:def 1;

now

assume r = q ; :: thesis: r,b // o,a'
then ( b,r // a,o & LIN o,a,a' ) by A2, A3, A18, A21, A24, A26, Def1, AFF_1:33;
then ( r,b // o,a & o,a // o,a' ) by AFF_1:13, AFF_1:def 1;
hence r,b // o,a' by A3, AFF_1:14; :: thesis: verum

end;

hence a',o // r,b by A33, A38, AFF_1:13, AFF_1:14; :: thesis: verum

end;

then A39: p,o // r,b' by A2, A3, A30, A31, A37, Def1;
then r,c' // r,b' by A25, A35, AFF_1:14;
then LIN r,c',b' by AFF_1:def 1;
then LIN c',b',r by AFF_1:15;
then c',b' // c',r by AFF_1:def 1;
then r,c' // b',c' by AFF_1:13;
then r = c' by A4, A36, AFF_1:14;
then p,o // b',c' by A39, AFF_1:13;
hence contradiction by A4, A25, A26, AFF_1:14; :: thesis: verum

end;

then A40: not b',c' // A by A3, A4, AFF_1:45;
set M = Line b',c';
set N = Line a',b';
set D = Line a',c';
A41: ( Line b',c' is being_line & Line a',b' is being_line & b' in Line b',c' & Line a',c' is being_line & c' in Line b',c' & a' in Line a',b' & b' in Line a',b' & a' in Line a',c' & c' in Line a',c' ) by A5, A8, A10, AFF_1:38;
then consider K being Subset of AP such that
A42: ( o in K & Line b',c' // K ) by AFF_1:63;
A43: ( K is being_line & K // Line b',c' ) by A42, AFF_1:50;
not Line a',b' // K

proof

assume Line a',b' // K ; :: thesis: contradiction
then Line a',b' // Line b',c' by A42, AFF_1:58;
then c' in Line a',b' by A41, AFF_1:59;
hence contradiction by A11, A41, AFF_1:33; :: thesis: verum

end;

then consider p being Element of AP such that
A44: ( p in Line a',b' & p in K ) by A41, A43, AFF_1:72;
consider T being Subset of AP such that
A45: ( p in T & Line a',c' // T ) by A41, AFF_1:63;
A46: ( T is being_line & T // Line a',c' ) by A45, AFF_1:50;
not C // T

proof

assume C // T ; :: thesis: contradiction
then C // Line a',c' by A45, AFF_1:58;
then a' in C by A3, A41, AFF_1:59;
hence contradiction by A3, A15, AFF_1:30; :: thesis: verum

end;

then consider q being Element of AP such that
A47: ( q in C & q in T ) by A3, A46, AFF_1:72;
A48: o <> p

proof

assume o = p ; :: thesis: contradiction
then ( LIN o,a',b' & LIN o,a',a & LIN o,a',a' ) by A3, A41, A44, AFF_1:33;
then ( b' in A & a',b' // a,b ) by A3, A15, AFF_1:13, AFF_1:39;
then ( b in A & b' in A ) by A3, A8, AFF_1:62;
hence contradiction by A3, AFF_1:30; :: thesis: verum

end;

A49: ( b',c' // p,o & p,q // a',c' ) by A41, A42, A44, A45, A47, AFF_1:53;
then A50: b',q // a',o by A2, A3, A41, A44, A47, Def1;
A51: p <> a

proof

assume p = a ; :: thesis: contradiction
then b' in A by A3, A7, A41, A44, AFF_1:30;
hence contradiction by A3, A16, AFF_1:30; :: thesis: verum

end;

A52: K <> A by A40, A41, A42, AFF_1:54;
A53: b' <> q

proof

assume b' = q ; :: thesis: contradiction
then P = C by A3, A16, A47, AFF_1:30;
hence contradiction by A3, A4, AFF_1:65; :: thesis: verum

end;

set R = Line a,p;
A54: ( Line a,p is being_line & a in Line a,p & p in Line a,p ) by A51, AFF_1:38;
not b',q // Line a,p

proof

assume b',q // Line a,p ; :: thesis: contradiction
then ( a',o // Line a,p & A // A ) by A3, A50, A53, AFF_1:46, AFF_1:55;
then ( a',o // Line a,p & a',o // A ) by A3, AFF_1:54;
then p in A by A3, A15, A54, AFF_1:59, AFF_1:67;
hence contradiction by A3, A42, A43, A44, A48, A52, AFF_1:30; :: thesis: verum

end;

then consider r being Element of AP such that
A55: ( r in Line a,p & LIN b',q,r ) by A54, AFF_1:73;
A56: p,q // a,c by A3, A10, A49, AFF_1:14;
A57: a,o // r,q

proof

LIN q,r,b' by A55, AFF_1:15;
then q,r // q,b' by AFF_1:def 1;
then r,q // b',q by AFF_1:13;
then A58: r,q // a',o by A50, A53, AFF_1:14;
LIN o,a,a' by A3, AFF_1:33;
then o,a // o,a' by AFF_1:def 1;
then a,o // a',o by AFF_1:13;
hence a,o // r,q by A15, A58, AFF_1:14; :: thesis: verum

end;

then A59: p,o // r,c by A2, A3, A47, A54, A55, A56, Def1;
then A60: b',c' // r,c by A48, A49, AFF_1:14;
A61: p,b' // a,b

proof

LIN b',a',p by A41, A44, AFF_1:33;
then b',a' // b',p by AFF_1:def 1;
then p,b' // a',b' by AFF_1:13;
hence p,b' // a,b by A3, A8, AFF_1:14; :: thesis: verum

end;

a,o // r,b'

proof

LIN r,b',q by A55, AFF_1:15;
then A62: r,b' // r,q by AFF_1:def 1;

now

assume r = q ; :: thesis: r,b' // o,a
then ( b',r // a',o & LIN o,a',a ) by A2, A3, A41, A44, A47, A49, Def1, AFF_1:33;
then ( r,b' // o,a' & o,a' // o,a ) by AFF_1:13, AFF_1:def 1;
hence r,b' // o,a by A15, AFF_1:14; :: thesis: verum

end;

hence a,o // r,b' by A57, A62, AFF_1:13, AFF_1:14; :: thesis: verum

end;

then A63: p,o // r,b by A2, A3, A54, A55, A61, Def1;
then r,c // r,b by A48, A59, AFF_1:14;
then LIN r,c,b by AFF_1:def 1;
then LIN c,b,r by AFF_1:15;
then c,b // c,r by AFF_1:def 1;
then b,c // r,c by AFF_1:13;
then r = c by A4, A60, AFF_1:14;
then b,c // p,o by A63, AFF_1:13;
hence contradiction by A4, A48, A49, AFF_1:14; :: thesis: verum

end;