let AP be AffinPlane; :: thesis: ( AP is satisfying_TDES_1 implies AP is satisfying_TDES_2 )
assume A1: AP is satisfying_TDES_1 ; :: thesis: AP is satisfying_TDES_2
thus AP is satisfying_TDES_2 :: thesis: verum

proof

let K be Subset of ; :: according to AFF_2:def 9 :: thesis: for o, a, b, c, a', b', c' being Element of st K is being_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & b,c // b',c' & a,c // a',c' & a,b // K holds
a,b // a',b'
let o, a, b, c, a', b', c' be Element of ; :: thesis: ( K is being_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & b,c // b',c' & a,c // a',c' & a,b // K implies a,b // a',b' )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c' in K and
A6: not a in K and
A7: o <> c and
A8: a <> b and
A9: LIN o,a,a' and
A10: LIN o,b,b' and
A11: b,c // b',c' and
A12: a,c // a',c' and
A13: a,b // K ; :: thesis: a,b // a',b'
set A = Line o,a;
set P = Line o,b;
A14: ( Line o,a is being_line & a in Line o,a ) by A3, A6, AFF_1:38;
A15: o in Line o,a by A3, A6, AFF_1:38;
then A16: a' in Line o,a by A3, A6, A9, A14, AFF_1:39;
A17: o <> b by A3, A6, A13, AFF_1:49;
then A18: Line o,b is being_line by AFF_1:38;
consider N being Subset of such that
A19: a' in N and
A20: K // N by A2, AFF_1:63;
A21: N is being_line by A20, AFF_1:50;
set T = Line b',c';
A22: not b in K by A6, A13, AFF_1:49;
A23: b in Line o,b by A17, AFF_1:38;
A24: o in Line o,b by A17, AFF_1:38;
then A25: b' in Line o,b by A10, A17, A18, A23, AFF_1:39;
assume A26: not a,b // a',b' ; :: thesis: contradiction
then A27: a' <> b' by AFF_1:12;
A28: not b' in K

proof

A29: a',c' // a,c by A12, AFF_1:13;
A30: b',c' // c,b by A11, AFF_1:13;
assume A31: b' in K ; :: thesis: contradiction
then b' = o by A2, A3, A22, A18, A24, A23, A25, AFF_1:30;
then c' in Line o,a by A2, A3, A4, A5, A22, A15, A30, AFF_1:62;
then ( a' = c' or c in Line o,a ) by A14, A16, A29, AFF_1:62;
hence contradiction by A2, A3, A4, A5, A6, A7, A27, A22, A15, A14, A31, A30, AFF_1:30, AFF_1:62; :: thesis: verum

end;

then A32: Line b',c' is being_line by A5, AFF_1:38;
A33: b' in Line b',c' by A5, A28, AFF_1:38;
A34: c' in Line b',c' by A5, A28, AFF_1:38;
not N // Line b',c'

proof

assume N // Line b',c' ; :: thesis: contradiction
then K // Line b',c' by A20, AFF_1:58;
hence contradiction by A5, A28, A33, A34, AFF_1:59; :: thesis: verum

end;

then consider x being Element of such that
A35: x in N and
A36: x in Line b',c' by A32, A21, AFF_1:72;
a',x // K by A19, A20, A35, AFF_1:54;
then A37: a,b // a',x by A2, A13, AFF_1:45;
LIN c',b',x by A32, A33, A34, A36, AFF_1:33;
then c',b' // c',x by AFF_1:def 1;
then b',c' // x,c' by AFF_1:13;
then b,c // x,c' by A5, A11, A28, AFF_1:14;
then LIN o,b,x by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A37, Def8;
then x in Line o,b by A17, A18, A24, A23, AFF_1:39;
then Line o,b = Line b',c' by A26, A18, A25, A32, A33, A36, A37, AFF_1:30;
then LIN c',b',b by A18, A23, A33, A34, AFF_1:33;
then c',b' // c',b by AFF_1:def 1;
then b',c' // b,c' by AFF_1:13;
then b,c // b,c' by A5, A11, A28, AFF_1:14;
then LIN b,c,c' by AFF_1:def 1;
then A38: LIN c,c',b by AFF_1:15;
then a,c // a',c by A2, A4, A5, A12, A22, AFF_1:39;
then c,a // c,a' by AFF_1:13;
then LIN c,a,a' by AFF_1:def 1;
then LIN a,a',c by AFF_1:15;
then A39: ( a = a' or c in Line o,a ) by A14, A16, AFF_1:39;
b,c // b',c by A2, A4, A5, A11, A22, A38, AFF_1:39;
then c,b // c,b' by AFF_1:13;
then LIN c,b,b' by AFF_1:def 1;
then LIN b,b',c by AFF_1:15;
then ( b = b' or c in Line o,b ) by A18, A23, A25, AFF_1:39;
hence contradiction by A2, A3, A4, A6, A7, A26, A22, A18, A15, A14, A24, A23, A39, AFF_1:11, AFF_1:30; :: thesis: verum

end;