let AP be AffinPlane; :: thesis:
assume A1: AP is satisfying_TDES_1 ; :: thesis:
thus AP is satisfying_des_1 :: thesis:

proof

let A be Subset of AP; :: according to AFF_2:def 12 :: thesis:
let P, C be Subset of AP; :: thesis:
let a, b, c, a9, b9, c9 be Element of AP; :: thesis:
assume that
A2: A // P and
A3: a in A and
A4: a9 in A and
A5: b in P and
A6: b9 in P and
A7: c in C and
A8: c9 in C and
A9: A is being_line and
A10: P is being_line and
A11: C is being_line and
A12: A <> P and
A13: A <> C and
A14: a,b // a9,b9 and
A15: a,c // a9,c9 and
A16: b,c // b9,c9 and
A17: not LIN a,b,c and
A18: c <> c9 ; :: thesis:
set P9 = Line a,b;
set C9 = Line a9,b9;
A19: a9 <> b9 by A2, A4, A6, A12, AFF_1:59;
then A20: a9 in Line a9,b9 by AFF_1:38;
A21: a9 <> c9

proof

assume a9 = c9 ; :: thesis:
then b,c // a9,b9 by A16, AFF_1:13;
then a,b // b,c by A14, A19, AFF_1:14;
then b,a // b,c by AFF_1:13;
then LIN b,a,c by AFF_1:def 1;
hence contradiction by A17, AFF_1:15; :: thesis:

end;

A22: not c9 in A

proof

assume A23: c9 in A ; :: thesis:
a9,c9 // a,c by A15, AFF_1:13;
then c in A by A3, A4, A9, A21, A23, AFF_1:62;
hence contradiction by A7, A8, A9, A11, A13, A18, A23, AFF_1:30; :: thesis:

end;

A24: Line a9,b9 is being_line by A19, AFF_1:38;
assume A25: not A // C ; :: thesis:
then consider o being Element of AP such that
A26: o in A and
A27: o in C by A9, A11, AFF_1:72;
A28: LIN o,c9,c by A7, A8, A11, A27, AFF_1:33;
A29: a <> a9

proof

assume A30: a = a9 ; :: thesis:
then LIN a,c,c9 by A15, AFF_1:def 1;
then A31: LIN c,c9,a by AFF_1:15;
LIN a,b,b9 by A14, A30, AFF_1:def 1;
then LIN b,b9,a by AFF_1:15;
then ( b = b9 or a in P ) by A5, A6, A10, AFF_1:39;
then LIN b,c,c9 by A2, A3, A12, A16, AFF_1:59, AFF_1:def 1;
then A32: LIN c,c9,b by AFF_1:15;
LIN c,c9,c by AFF_1:16;
hence contradiction by A17, A18, A31, A32, AFF_1:17; :: thesis:

end;

A33: o <> a9

proof

assume A34: o = a9 ; :: thesis:
a9,c9 // c,a by A15, AFF_1:13;
then a in C by A7, A8, A11, A27, A21, A34, AFF_1:62;
hence contradiction by A3, A4, A9, A11, A13, A27, A29, A34, AFF_1:30; :: thesis:

end;

A35: a <> b by A17, AFF_1:16;
then A36: Line a,b is being_line by AFF_1:38;
consider N being Subset of AP such that
A37: c9 in N and
A38: A // N by A9, AFF_1:63;
A39: b9 in Line a9,b9 by A19, AFF_1:38;
A40: not N // Line a9,b9

proof

assume N // Line a9,b9 ; :: thesis:
then A // Line a9,b9 by A38, AFF_1:58;
then b9 in A by A4, A39, A20, AFF_1:59;
hence contradiction by A2, A6, A12, AFF_1:59; :: thesis:

end;

N is being_line by A38, AFF_1:50;
then consider q being Element of AP such that
A41: q in N and
A42: q in Line a9,b9 by A24, A40, AFF_1:72;
A43: c9,q // A by A37, A38, A41, AFF_1:54;
A44: c9 <> q

proof

assume c9 = q ; :: thesis:
then LIN a9,b9,c9 by A24, A39, A20, A42, AFF_1:33;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a9,b9 // a,c by A15, A21, AFF_1:14;
then a,b // a,c by A14, A19, AFF_1:14;
hence contradiction by A17, AFF_1:def 1; :: thesis:

end;

A45: c9,a9 // c,a by A15, AFF_1:13;
A46: c,b // c9,b9 by A16, AFF_1:13;
A47: a in Line a,b by A35, AFF_1:38;
A48: b <> c by A17, AFF_1:16;
A49: not c in P

proof

assume A50: c in P ; :: thesis:
then c9 in P by A5, A6, A10, A16, A48, AFF_1:62;
hence contradiction by A2, A7, A8, A10, A11, A18, A25, A50, AFF_1:30; :: thesis:

end;

not P // C by A2, A25, AFF_1:58;
then consider s being Element of AP such that
A51: s in P and
A52: s in C by A10, A11, AFF_1:72;
A53: LIN s,c,c9 by A7, A8, A11, A52, AFF_1:33;
A54: b <> b9

proof

assume b = b9 ; :: thesis:
then b,a // b,a9 by A14, AFF_1:13;
then LIN b,a,a9 by AFF_1:def 1;
then LIN a,a9,b by AFF_1:15;
then b in A by A3, A4, A9, A29, AFF_1:39;
hence contradiction by A2, A5, A12, AFF_1:59; :: thesis:

end;

A55: s <> b

proof

assume A56: s = b ; :: thesis:
b,c // c9,b9 by A16, AFF_1:13;
then b9 in C by A7, A8, A11, A48, A52, A56, AFF_1:62;
hence contradiction by A2, A5, A6, A10, A11, A25, A54, A52, A56, AFF_1:30; :: thesis:

end;

consider M being Subset of AP such that
A57: c in M and
A58: A // M by A9, AFF_1:63;
A59: M is being_line by A58, AFF_1:50;
A60: b in Line a,b by A35, AFF_1:38;
not M // Line a,b

proof

assume M // Line a,b ; :: thesis:
then A // Line a,b by A58, AFF_1:58;
then b in A by A3, A60, A47, AFF_1:59;
hence contradiction by A2, A5, A12, AFF_1:59; :: thesis:

end;

then consider p being Element of AP such that
A61: p in M and
A62: p in Line a,b by A59, A36, AFF_1:72;
M // P by A2, A58, AFF_1:58;
then A63: c,p // P by A57, A61, AFF_1:54;
A64: M // N by A58, A38, AFF_1:58;
then A65: c,p // c9,q by A57, A37, A61, A41, AFF_1:53;

A66: now

assume p = q ; :: thesis:
then M = N by A64, A61, A41, AFF_1:59;
hence contradiction by A7, A8, A11, A18, A25, A57, A58, A37, A59, AFF_1:30; :: thesis:

end;

A67: Line a,b // Line a9,b9 by A14, A35, A19, AFF_1:51;
then A68: p,b // q,b9 by A60, A39, A62, A42, AFF_1:53;
A69: q,a9 // p,a by A47, A20, A67, A62, A42, AFF_1:53;
c9,q // c,p by A57, A37, A64, A61, A41, AFF_1:53;
then LIN o,q,p by A1, A3, A4, A9, A26, A28, A22, A45, A69, A43, A44, A33, Def8;
then A70: LIN p,q,o by AFF_1:15;
c <> p by A17, A36, A60, A47, A62, AFF_1:33;
then LIN s,p,q by A1, A5, A6, A10, A51, A53, A63, A68, A49, A55, A65, A46, Def8;
then A71: LIN p,q,s by AFF_1:15;
LIN p,q,p by AFF_1:16;
then ( o = s or p in C ) by A11, A27, A52, A70, A71, A66, AFF_1:17, AFF_1:39;
then c in Line a,b by A2, A7, A11, A12, A25, A26, A57, A58, A59, A61, A62, A51, AFF_1:30, AFF_1:59;
hence contradiction by A17, A36, A60, A47, AFF_1:33; :: thesis:

end;