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 ; :: according to AFF_2:def 12 :: thesis:
let P, C be Subset of ; :: thesis:
let a, b, c, a', b', c' be Element of ; :: thesis:
assume that
A2: A // P and
A3: a in A and
A4: a' in A and
A5: b in P and
A6: b' in P and
A7: c in C and
A8: c' 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 // a',b' and
A15: a,c // a',c' and
A16: b,c // b',c' and
A17: not LIN a,b,c and
A18: c <> c' ; :: thesis:
set P' = Line a,b;
set C' = Line a',b';
A19: a' <> b' by A2, A4, A6, A12, AFF_1:59;
then A20: a' in Line a',b' by AFF_1:38;
A21: a' <> c'

proof

assume a' = c' ; :: thesis:
then b,c // a',b' 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 c' in A

proof

assume A23: c' in A ; :: thesis:
a',c' // 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 a',b' is being_line by A19, AFF_1:38;
assume A25: not A // C ; :: thesis:
then consider o being Element of such that
A26: o in A and
A27: o in C by A9, A11, AFF_1:72;
A28: LIN o,c',c by A7, A8, A11, A27, AFF_1:33;
A29: a <> a'

proof

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

end;

A33: o <> a'

proof

assume A34: o = a' ; :: thesis:
a',c' // 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 such that
A37: c' in N and
A38: A // N by A9, AFF_1:63;
A39: b' in Line a',b' by A19, AFF_1:38;
A40: not N // Line a',b'

proof

assume N // Line a',b' ; :: thesis:
then A // Line a',b' by A38, AFF_1:58;
then b' 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 such that
A41: q in N and
A42: q in Line a',b' by A24, A40, AFF_1:72;
A43: c',q // A by A37, A38, A41, AFF_1:54;
A44: c' <> q

proof

assume c' = q ; :: thesis:
then LIN a',b',c' by A24, A39, A20, A42, AFF_1:33;
then a',b' // a',c' by AFF_1:def 1;
then a',b' // 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: c',a' // c,a by A15, AFF_1:13;
A46: c,b // c',b' 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 c' 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 such that
A51: s in P and
A52: s in C by A10, A11, AFF_1:72;
A53: LIN s,c,c' by A7, A8, A11, A52, AFF_1:33;
A54: b <> b'

proof

assume b = b' ; :: thesis:
then b,a // b,a' by A14, AFF_1:13;
then LIN b,a,a' by AFF_1:def 1;
then LIN a,a',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 // c',b' by A16, AFF_1:13;
then b' 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 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 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 // c',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 a',b' by A14, A35, A19, AFF_1:51;
then A68: p,b // q,b' by A60, A39, A62, A42, AFF_1:53;
A69: q,a' // p,a by A47, A20, A67, A62, A42, AFF_1:53;
c',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;