let AP be AffinPlane; :: thesis: ( AP is satisfying_DES1_2 implies AP is Desarguesian )
assume A1: AP is satisfying_DES1_2 ; :: thesis: AP is Desarguesian
let A be Subset of AP; :: according to AFF_2:def 4 :: thesis: for b₁, b₂ being M2(K10(the carrier of AP))
for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being M2(the carrier of AP) holds
( not b₃ in A or not b₃ in b₁ or not b₃ in b₂ or b₃ = b₄ or b₃ = b₅ or b₃ = b₆ or not b₄ in A or not b₇ in A or not b₅ in b₁ or not b₈ in b₁ or not b₆ in b₂ or not b₉ in b₂ or not A is being_line or not b₁ is being_line or not b₂ is being_line or A = b₁ or A = b₂ or not b₄,b₅ // b₇,b₈ or not b₄,b₆ // b₇,b₉ or b₅,b₆ // b₈,b₉ )
let P, C be Subset of AP; :: thesis: for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being M2(the carrier of AP) holds
( not b₁ in A or not b₁ in P or not b₁ in C or b₁ = b₂ or b₁ = b₃ or b₁ = b₄ or not b₂ in A or not b₅ in A or not b₃ in P or not b₆ in P or not b₄ in C or not b₇ in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not b₂,b₃ // b₅,b₆ or not b₂,b₄ // b₅,b₇ or b₃,b₄ // b₆,b₇ )
let o, a, b, c, a', b', c' be Element of AP; :: thesis: ( not o in A or not o in P or not o in C or o = a or o = b or o = c or not a in A or not a' in A or not b in P or not b' in P or not c in C or not c' in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not a,b // a',b' or not a,c // a',c' or b,c // b',c' )
assume that
A2: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C ) and
A3: ( A is being_line & P is being_line & C is being_line ) and
A4: ( A <> P & A <> C ) and
A5: ( a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'

now

assume A6: P <> C ; :: thesis: b,c // b',c'
then A7: ( a <> b & a <> c & b <> c ) by A2, A3, A4, AFF_1:30;
A8: ( not LIN o,b,a & not LIN o,a,c )

proof

assume A9: ( LIN o,b,a or LIN o,a,c ) ; :: thesis: contradiction

A10: now

assume LIN o,b,a ; :: thesis: contradiction
then a in P by A2, A3, AFF_1:39;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

now

assume LIN o,a,c ; :: thesis: contradiction
then c in A by A2, A3, AFF_1:39;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

hence contradiction by A9, A10; :: thesis: verum

end;

A11: ( a' = o implies b,c // b',c' )

proof

assume A12: a' = o ; :: thesis: b,c // b',c'
( LIN o,a,a' & LIN o,c,c' & not LIN o,a,c ) by A2, A3, A8, AFF_1:33;
then A13: o = c' by A5, A12, AFF_1:69;
( LIN o,a,a' & LIN o,b,b' & not LIN o,a,b ) by A2, A3, A8, AFF_1:15, AFF_1:33;
then o = b' by A5, A12, AFF_1:69;
hence b,c // b',c' by A13, AFF_1:12; :: thesis: verum

end;

A14: ( b' = o implies b,c // b',c' )

proof

assume A15: b' = o ; :: thesis: b,c // b',c'
( LIN o,b,b' & LIN o,a,a' & not LIN o,b,a & b,a // b',a' ) by A2, A3, A5, A8, AFF_1:13, AFF_1:33;
hence b,c // b',c' by A11, A15, AFF_1:69; :: thesis: verum

end;

A16: ( c' = o implies b,c // b',c' )

proof

assume A17: c' = o ; :: thesis: b,c // b',c'
( LIN o,c,c' & LIN o,a,a' & not LIN o,c,a & c,a // c',a' ) by A2, A3, A5, A8, AFF_1:13, AFF_1:15, AFF_1:33;
hence b,c // b',c' by A11, A17, AFF_1:69; :: thesis: verum

end;

set K = Line a,c;
A18: ( Line a,c is being_line & a in Line a,c & c in Line a,c ) by A7, AFF_1:26, AFF_1:def 3;
A19: ( LIN a,b,c implies b,c // b',c' )

proof

assume LIN a,b,c ; :: thesis: b,c // b',c'
then LIN a,c,b by AFF_1:15;
then A20: b in Line a,c by AFF_1:def 2;
then ( Line a,c = Line a,b & Line a,c = Line b,c ) by A7, A18, AFF_1:71;
then A21: ( a',c' // Line a,c & a',b' // Line a,c ) by A5, A7, AFF_1:43, AFF_1:46;
consider N being Subset of AP such that
A22: ( a' in N & Line a,c // N ) by A18, AFF_1:63;
A23: N is being_line by A22, AFF_1:50;
( a',c' // N & a',b' // N ) by A21, A22, AFF_1:57;
then ( c' in N & b' in N ) by A22, A23, AFF_1:37;
hence b,c // b',c' by A18, A20, A22, AFF_1:53; :: thesis: verum

end;

A24: ( b = b' implies b,c // b',c' )

proof

assume A25: b = b' ; :: thesis: b,c // b',c'
then ( LIN o,a,a' & not LIN o,b,a & b,a // b,a' ) by A2, A3, A5, A8, AFF_1:13, AFF_1:33;
then ( LIN o,c,c' & not LIN o,a,c & a,c // a,c' ) by A2, A3, A5, A8, AFF_1:23, AFF_1:33;
then c = c' by AFF_1:23;
hence b,c // b',c' by A25, AFF_1:11; :: thesis: verum

end;

now

assume A26: ( o <> a' & o <> b' & o <> c' & b <> b' & not LIN a,b,c ) ; :: thesis: b,c // b',c'
then A27: ( a' <> b' & a' <> c' & b' <> c' ) by A2, A3, A4, A6, AFF_1:30;
assume not b,c // b',c' ; :: thesis: contradiction
then consider q being Element of AP such that
A28: ( LIN b,c,q & LIN b',c',q ) by AFF_1:74;
consider M being Subset of AP such that
A29: ( q in M & Line a,c // M ) by A18, AFF_1:63;
A30: M is being_line by A29, AFF_1:50;
not a,b // M

proof

assume a,b // M ; :: thesis: contradiction
then a,b // Line a,c by A29, AFF_1:57;
then b in Line a,c by A18, AFF_1:37;
hence contradiction by A18, A26, AFF_1:33; :: thesis: verum

end;

then consider p being Element of AP such that
A31: ( p in M & LIN a,b,p ) by A30, AFF_1:73;
set N = Line a',c';
A32: ( Line a',c' is being_line & a' in Line a',c' & c' in Line a',c' ) by A27, AFF_1:26, AFF_1:def 3;
A33: Line a,c // Line a',c' by A5, A7, A27, AFF_1:51;
then A34: Line a',c' // M by A29, AFF_1:58;
A35: not LIN a',b',c'

proof

assume LIN a',b',c' ; :: thesis: contradiction
then LIN a',c',b' by AFF_1:15;
then b' in Line a',c' by AFF_1:def 2;
then a',b' // Line a',c' by A32, AFF_1:37;
then A36: a',b' // Line a,c by A33, AFF_1:57;
a',b' // a,b by A5, AFF_1:13;
then a,b // Line a,c by A27, A36, AFF_1:46;
then b in Line a,c by A18, AFF_1:37;
hence contradiction by A18, A26, AFF_1:33; :: thesis: verum

end;

A37: a <> a'

proof

assume a = a' ; :: thesis: contradiction
then ( not LIN o,a,b & LIN o,b,b' & a,b // a,b' ) by A2, A3, A5, A8, AFF_1:15, AFF_1:33;
hence contradiction by A26, AFF_1:23; :: thesis: verum

end;

A38: c <> c'

proof

assume c = c' ; :: thesis: contradiction
then ( not LIN o,c,a & LIN o,a,a' & c,a // c,a' ) by A2, A3, A5, A8, AFF_1:13, AFF_1:15, AFF_1:33;
hence contradiction by A37, AFF_1:23; :: thesis: verum

end;

A39: A <> Line a,c by A2, A3, A4, A18, AFF_1:30;
not b',p // Line a',c'

proof

assume b',p // Line a',c' ; :: thesis: contradiction
then b',p // M by A34, AFF_1:57;
then p,b' // M by AFF_1:48;
then A40: b' in M by A30, A31, AFF_1:37;

A41: now

assume b' = q ; :: thesis: contradiction
then LIN b,b',c by A28, AFF_1:15;
then c in P by A2, A3, A26, AFF_1:39;
hence contradiction by A2, A3, A6, AFF_1:30; :: thesis: verum

end;

now

assume A42: b' <> q ; :: thesis: contradiction
LIN b',q,c' by A28, AFF_1:15;
then c' in M by A29, A30, A40, A42, AFF_1:39;
then ( a' in Line a',c' & b' in Line a',c' & c' in Line a',c' ) by A32, A34, A40, AFF_1:59;
hence contradiction by A32, A35, AFF_1:33; :: thesis: verum

end;

hence contradiction by A41; :: thesis: verum

end;

then consider x being Element of AP such that
A43: ( x in Line a',c' & LIN b',p,x ) by A32, AFF_1:73;
A44: LIN b',x,p by A43, AFF_1:15;
A45: x <> a

proof

assume x = a ; :: thesis: contradiction
then ( a in Line a,c & a' in Line a,c ) by A18, A32, A33, A43, AFF_1:59;
then A = Line a,c by A2, A3, A18, A37, AFF_1:30;
hence contradiction by A2, A3, A4, A18, AFF_1:30; :: thesis: verum

end;

set A' = Line x,a;
A46: ( Line x,a is being_line & x in Line x,a & a in Line x,a ) by A45, AFF_1:26, AFF_1:def 3;
A47: p <> q

proof

assume A48: p = q ; :: thesis: contradiction
then ( LIN p,b,c & LIN p,b,a & LIN p,b,b ) by A28, A31, AFF_1:15, AFF_1:16;
then p = b by A26, AFF_1:17;
then LIN b,b',c' by A28, A48, AFF_1:15;
then c' in P by A2, A3, A26, AFF_1:39;
hence contradiction by A2, A3, A6, A26, AFF_1:30; :: thesis: verum

end;

A49: not LIN b',c',x

proof

assume LIN b',c',x ; :: thesis: contradiction
then A50: ( LIN c',x,b' & LIN c',x,a' & LIN c',x,c' ) by A32, A43, AFF_1:15, AFF_1:33;
then A51: ( c' = x or LIN b',c',a' ) by AFF_1:17;

A52: now

assume c' = x ; :: thesis: LIN b',c',a'
then ( LIN b',c',p & LIN b',c',c' ) by A43, AFF_1:15, AFF_1:16;
then c' in M by A27, A28, A29, A30, A31, A47, AFF_1:17, AFF_1:39;
then ( q in Line a',c' & LIN q,c',b' ) by A28, A29, A32, A34, AFF_1:15, AFF_1:59;
then A53: ( q = c' or b' in Line a',c' ) by A32, AFF_1:39;

now

assume q = c' ; :: thesis: contradiction
then LIN c,c',b by A28, AFF_1:15;
then b in C by A2, A3, A38, AFF_1:39;
hence contradiction by A2, A3, A6, AFF_1:30; :: thesis: verum

end;

hence LIN b',c',a' by A32, A53, AFF_1:33; :: thesis: verum

end;

then b',c' // b',a' by A51, AFF_1:def 1;
then b',c' // a',b' by AFF_1:13;
then A54: b',c' // a,b by A5, A27, AFF_1:14;
LIN c',a',b' by A50, A52, AFF_1:15, AFF_1:17;
then c',a' // c',b' by AFF_1:def 1;
then a',c' // b',c' by AFF_1:13;
then a,c // b',c' by A5, A27, AFF_1:14;
then a,c // a,b by A27, A54, AFF_1:14;
then LIN a,c,b by AFF_1:def 1;
hence contradiction by A26, AFF_1:15; :: thesis: verum

end;

A55: c,a // c',x by A18, A32, A33, A43, AFF_1:53;
A56: c,a // q,p by A18, A29, A31, AFF_1:53;
( not LIN b,c,a & LIN b,a,p ) by A26, A31, AFF_1:15;
then o in Line x,a by A1, A2, A3, A6, A28, A44, A45, A46, A47, A49, A55, A56, Def3;
then A57: x in A by A2, A3, A46, AFF_1:30;
A <> Line a',c' by A2, A18, A33, A39, AFF_1:59;
then A58: x = a' by A2, A3, A32, A43, A57, AFF_1:30;
set D = Line b,a;
set T = Line b',a';
A59: ( Line b,a is being_line & Line b',a' is being_line & b in Line b,a & a in Line b,a & p in Line b,a & b' in Line b',a' & a' in Line b',a' & p in Line b',a' ) by A7, A27, A31, A44, A58, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
Line b,a // Line b',a' by A5, A7, A27, AFF_1:51;
then ( a in Line b,a & a' in Line b,a ) by A59, AFF_1:59;
then b in A by A2, A3, A37, A59, AFF_1:30;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

hence b,c // b',c' by A11, A14, A16, A19, A24; :: thesis: verum

end;

hence b,c // b',c' by A2, A3, AFF_1:65; :: thesis: verum