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 U1 of AP))
for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being M2(the U1 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 U1 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, a9, b9, c9 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 a9 in A or not b in P or not b9 in P or not c in C or not c9 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 // a9,b9 or not a,c // a9,c9 or b,c // 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 ; :: thesis: b,c // b9,c9

now

A21: ( not LIN o,b,a & not LIN o,a,c )

proof

A22: now

assume LIN o,a,c ; :: thesis: contradiction
then c in A by A2, A5, A8, A14, AFF_1:39;
hence contradiction by A2, A4, A7, A12, A14, A16, A18, AFF_1:30; :: thesis: verum

end;

A23: now

assume LIN o,b,a ; :: thesis: contradiction
then a in P by A3, A6, A10, A15, AFF_1:39;
hence contradiction by A2, A3, A5, A8, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

assume ( LIN o,b,a or LIN o,a,c ) ; :: thesis: contradiction
hence contradiction by A23, A22; :: thesis: verum

end;

A24: ( b = b9 implies b,c // b9,c9 )

proof

A25: LIN o,c,c9 by A4, A12, A13, A16, AFF_1:33;
A26: LIN o,a,a9 by A2, A8, A9, A14, AFF_1:33;
assume A27: b = b9 ; :: thesis: b,c // b9,c9
then b,a // b,a9 by A19, AFF_1:13;
then a,c // a,c9 by A20, A21, A26, AFF_1:23;
then c = c9 by A21, A25, AFF_1:23;
hence b,c // b9,c9 by A27, AFF_1:11; :: thesis: verum

end;

A28: ( a9 = o implies b,c // b9,c9 )

proof

assume A29: a9 = o ; :: thesis: b,c // b9,c9
( LIN o,b,b9 & not LIN o,a,b ) by A3, A10, A11, A15, A21, AFF_1:15, AFF_1:33;
then A30: o = b9 by A19, A29, AFF_1:69;
LIN o,c,c9 by A4, A12, A13, A16, AFF_1:33;
then o = c9 by A20, A21, A29, AFF_1:69;
hence b,c // b9,c9 by A30, AFF_1:12; :: thesis: verum

end;

A31: ( c9 = o implies b,c // b9,c9 )

proof

A32: c,a // c9,a9 by A20, AFF_1:13;
assume A33: c9 = o ; :: thesis: b,c // b9,c9
( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A14, A21, AFF_1:15, AFF_1:33;
hence b,c // b9,c9 by A28, A33, A32, AFF_1:69; :: thesis: verum

end;

set K = Line a,c;
A34: a in Line a,c by AFF_1:26;
A35: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1:30;
then A36: Line a,c is being_line by AFF_1:def 3;
A37: c in Line a,c by AFF_1:26;
A38: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1:30;
A39: ( LIN a,b,c implies b,c // b9,c9 )

proof

consider N being Subset of AP such that
A40: a9 in N and
A41: Line a,c // N by A36, AFF_1:63;
A42: N is being_line by A41, AFF_1:50;
a9,c9 // Line a,c by A20, A35, AFF_1:43, AFF_1:46;
then a9,c9 // N by A41, AFF_1:57;
then A43: c9 in N by A40, A42, AFF_1:37;
assume LIN a,b,c ; :: thesis: b,c // b9,c9
then LIN a,c,b by AFF_1:15;
then A44: b in Line a,c by AFF_1:def 2;
then Line a,c = Line a,b by A38, A36, A34, AFF_1:71;
then a9,b9 // Line a,c by A19, A38, AFF_1:43, AFF_1:46;
then a9,b9 // N by A41, AFF_1:57;
then b9 in N by A40, A42, AFF_1:37;
hence b,c // b9,c9 by A37, A44, A41, A43, AFF_1:53; :: thesis: verum

end;

assume A45: P <> C ; :: thesis: b,c // b9,c9

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 ; :: thesis: b,c // b9,c9
A52: c9 in Line a9,c9 by AFF_1:26;
assume not b,c // b9,c9 ; :: thesis: contradiction
then consider q being Element of AP such that
A53: LIN b,c,q and
A54: LIN b9,c9,q by AFF_1:74;
consider M being Subset of AP such that
A55: q in M and
A56: Line a,c // M by A36, AFF_1:63;
A57: M is being_line by A56, AFF_1:50;
not a,b // M

proof

assume a,b // M ; :: thesis: contradiction
then a,b // Line a,c by A56, AFF_1:57;
then b in Line a,c by A36, A34, AFF_1:37;
hence contradiction by A36, A34, A37, A51, AFF_1:33; :: thesis: verum

end;

then consider p being Element of AP such that
A58: p in M and
A59: LIN a,b,p by A57, AFF_1:73;
A60: a9 in Line a9,c9 by AFF_1:26;
A61: p <> q

proof

A62: ( LIN p,b,a & LIN p,b,b ) by A59, AFF_1:15, AFF_1:16;
assume A63: p = q ; :: thesis: contradiction
then LIN p,b,c by A53, AFF_1:15;
then p = b by A51, A62, AFF_1:17;
then LIN b,b9,c9 by A54, A63, AFF_1:15;
then c9 in P by A10, A11, A15, A50, AFF_1:39;
hence contradiction by A3, A4, A13, A15, A16, A45, A49, AFF_1:30; :: thesis: verum

end;

A64: c,a // q,p by A34, A37, A55, A56, A58, AFF_1:53;
A65: LIN b,a,p by A59, AFF_1:15;
A66: b9 <> c9 by A3, A4, A11, A13, A15, A16, A45, A48, AFF_1:30;
A67: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A47, AFF_1:30;
then A68: Line a9,c9 is being_line by AFF_1:def 3;
A69: Line a,c // Line a9,c9 by A20, A35, A67, AFF_1:51;
then A70: Line a9,c9 // M by A56, AFF_1:58;
A71: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A47, AFF_1:30;
A72: not LIN a9,b9,c9

proof

assume LIN a9,b9,c9 ; :: thesis: contradiction
then LIN a9,c9,b9 by AFF_1:15;
then b9 in Line a9,c9 by AFF_1:def 2;
then a9,b9 // Line a9,c9 by A68, A60, AFF_1:37;
then A73: a9,b9 // Line a,c by A69, AFF_1:57;
a9,b9 // a,b by A19, AFF_1:13;
then a,b // Line a,c by A71, A73, AFF_1:46;
then b in Line a,c by A36, A34, AFF_1:37;
hence contradiction by A36, A34, A37, A51, AFF_1:33; :: thesis: verum

end;

not b9,p // Line a9,c9

proof

assume b9,p // Line a9,c9 ; :: thesis: contradiction
then b9,p // M by A70, AFF_1:57;
then p,b9 // M by AFF_1:48;
then A74: b9 in M by A57, A58, AFF_1:37;

A75: now

assume A76: b9 <> q ; :: thesis: contradiction
LIN b9,q,c9 by A54, AFF_1:15;
then c9 in M by A55, A57, A74, A76, AFF_1:39;
then ( a9 in Line a9,c9 & b9 in Line a9,c9 ) by A52, A70, A74, AFF_1:26, AFF_1:59;
hence contradiction by A68, A52, A72, AFF_1:33; :: thesis: verum

end;

now

assume b9 = q ; :: thesis: contradiction
then LIN b,b9,c by A53, AFF_1:15;
then c in P by A10, A11, A15, A50, AFF_1:39;
hence contradiction by A3, A4, A7, A12, A15, A16, A45, AFF_1:30; :: thesis: verum

end;

hence contradiction by A75; :: thesis: verum

end;

then consider x being Element of AP such that
A77: x in Line a9,c9 and
A78: LIN b9,p,x by A68, AFF_1:73;
set A9 = Line x,a;
A79: a <> a9

proof

assume A80: a = a9 ; :: thesis: contradiction
( not LIN o,a,b & LIN o,b,b9 ) by A3, A10, A11, A15, A21, AFF_1:15, AFF_1:33;
hence contradiction by A19, A50, A80, AFF_1:23; :: thesis: verum

end;

A81: x <> a

proof

assume x = a ; :: thesis: contradiction
then a9 in Line a,c by A34, A60, A69, A77, AFF_1:59;
then A = Line a,c by A8, A9, A14, A36, A34, A79, AFF_1:30;
hence contradiction by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:30; :: thesis: verum

end;

then A82: Line x,a is being_line by AFF_1:def 3;
A83: c <> c9

proof

assume c = c9 ; :: thesis: contradiction
then A84: c,a // c,a9 by A20, AFF_1:13;
( not LIN o,c,a & LIN o,a,a9 ) by A2, A8, A9, A14, A21, AFF_1:15, AFF_1:33;
hence contradiction by A79, A84, AFF_1:23; :: thesis: verum

end;

A85: not LIN b9,c9,x

proof

A86: now

A87: now

assume q = c9 ; :: thesis: contradiction
then LIN c,c9,b by A53, AFF_1:15;
then b in C by A12, A13, A16, A83, AFF_1:39;
hence contradiction by A3, A4, A6, A10, A15, A16, A45, AFF_1:30; :: thesis: verum

end;

assume c9 = x ; :: thesis: LIN b9,c9,a9
then A88: LIN b9,c9,p by A78, AFF_1:15;
LIN b9,c9,c9 by AFF_1:16;
then c9 in M by A66, A54, A55, A57, A58, A61, A88, AFF_1:17, AFF_1:39;
then A89: q in Line a9,c9 by A55, A52, A70, AFF_1:59;
LIN q,c9,b9 by A54, AFF_1:15;
then ( q = c9 or b9 in Line a9,c9 ) by A68, A52, A89, AFF_1:39;
hence LIN b9,c9,a9 by A68, A60, A52, A87, AFF_1:33; :: thesis: verum

end;

assume LIN b9,c9,x ; :: thesis: contradiction
then A90: LIN c9,x,b9 by AFF_1:15;
A91: ( LIN c9,x,a9 & LIN c9,x,c9 ) by A68, A60, A52, A77, AFF_1:33;
then LIN c9,a9,b9 by A90, A86, AFF_1:15, AFF_1:17;
then c9,a9 // c9,b9 by AFF_1:def 1;
then a9,c9 // b9,c9 by AFF_1:13;
then A92: a,c // b9,c9 by A20, A67, AFF_1:14;
( c9 = x or LIN b9,c9,a9 ) by A90, A91, AFF_1:17;
then b9,c9 // b9,a9 by A86, AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:13;
then b9,c9 // a,b by A19, A71, AFF_1:14;
then a,c // a,b by A66, A92, AFF_1:14;
then LIN a,c,b by AFF_1:def 1;
hence contradiction by A51, AFF_1:15; :: thesis: verum

end;

A93: ( x in Line x,a & a in Line x,a ) by AFF_1:26;
A <> Line a,c by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:30;
then A94: A <> Line a9,c9 by A8, A34, A69, AFF_1:59;
A95: not LIN b,c,a by A51, AFF_1:15;
A96: p in Line b,a by A59, AFF_1:def 2;
A97: ( Line b,a is being_line & b in Line b,a ) by A38, AFF_1:26, AFF_1:def 3;
A98: LIN b9,x,p by A78, AFF_1:15;
c,a // c9,x by A34, A37, A52, A69, A77, AFF_1:53;
then o in Line x,a by A1, A3, A4, A6, A7, A10, A11, A12, A13, A15, A16, A45, A53, A54, A98, A81, A82, A93, A61, A85, A64, A95, A65, Def3;
then x in A by A2, A5, A8, A14, A82, A93, AFF_1:30;
then x = a9 by A9, A14, A68, A60, A77, A94, AFF_1:30;
then A99: ( a9 in Line b9,a9 & p in Line b9,a9 ) by A98, AFF_1:26, AFF_1:def 2;
Line b,a // Line b9,a9 by A19, A38, A71, AFF_1:51;
then ( a in Line b,a & a9 in Line b,a ) by A96, A99, AFF_1:26, AFF_1:59;
then b in A by A8, A9, A14, A79, A97, AFF_1:30;
hence contradiction by A2, A3, A6, A10, A14, A15, A17, AFF_1:30; :: thesis: verum

end;

( b9 = o implies b,c // b9,c9 )

proof

assume A100: b9 = o ; :: thesis: b,c // b9,c9
( LIN o,a,a9 & b,a // b9,a9 ) by A2, A8, A9, A14, A19, AFF_1:13, AFF_1:33;
hence b,c // b9,c9 by A21, A28, A100, AFF_1:69; :: thesis: verum

end;

hence b,c // b9,c9 by A28, A31, A39, A24, A46; :: thesis: verum

end;

hence b,c // b9,c9 by A10, A11, A12, A13, A15, AFF_1:65; :: thesis: verum