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 AP; :: according to AFF_2:def 9 :: thesis: for o, a, b, c, a', b', c' being Element of AP 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 AP; :: 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 A2: ( 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 ) ; :: thesis: a,b // a',b'
assume A3: not a,b // a',b' ; :: thesis: contradiction
then A4: a' <> b' by AFF_1:12;
A5: not b in K by A2, AFF_1:49;
A6: ( o <> a & o <> b ) by A2, AFF_1:49;
set A = Line o,a;
set P = Line o,b;
A7: ( Line o,a is being_line & Line o,b is being_line & o in Line o,a & a in Line o,a & o in Line o,b & b in Line o,b ) by A6, AFF_1:38;
then A8: ( a' in Line o,a & b' in Line o,b ) by A2, A6, AFF_1:39;
A9: not b' in K

proof

assume A10: b' in K ; :: thesis: contradiction
then A11: b' = o by A2, A5, A7, A8, AFF_1:30;
A12: b',c' // c,b by A2, AFF_1:13;
then ( c' in Line o,a & a',c' // a,c ) by A2, A5, A7, A11, AFF_1:13, AFF_1:62;
then ( a' = c' or c in Line o,a ) by A7, A8, AFF_1:62;
hence contradiction by A2, A4, A5, A7, A10, A12, AFF_1:30, AFF_1:62; :: thesis: verum

end;

set T = Line b',c';
A13: ( Line b',c' is being_line & b' in Line b',c' & c' in Line b',c' ) by A2, A9, AFF_1:38;
consider N being Subset of AP such that
A14: ( a' in N & K // N ) by A2, AFF_1:63;
A15: ( N is being_line & N // K ) by A14, AFF_1:50;
not N // Line b',c'

proof

assume N // Line b',c' ; :: thesis: contradiction
then K // Line b',c' by A14, AFF_1:58;
hence contradiction by A2, A9, A13, AFF_1:59; :: thesis: verum

end;

then consider x being Element of AP such that
A16: ( x in N & x in Line b',c' ) by A13, A15, AFF_1:72;
a',x // K by A14, A16, AFF_1:54;
then A17: a,b // a',x by A2, AFF_1:45;
b,c // x,c'

proof

LIN c',b',x by A13, A16, AFF_1:33;
then c',b' // c',x by AFF_1:def 1;
then b',c' // x,c' by AFF_1:13;
hence b,c // x,c' by A2, A9, AFF_1:14; :: thesis: verum

end;

then LIN o,b,x by A1, A2, A17, Def8;
then x in Line o,b by A6, A7, AFF_1:39;
then Line o,b = Line b',c' by A3, A7, A8, A13, A16, A17, AFF_1:30;
then LIN c',b',b by A7, A13, 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 A2, A9, AFF_1:14;
then LIN b,c,c' by AFF_1:def 1;
then LIN c,c',b by AFF_1:15;
then ( a,c // a',c & b,c // b',c ) by A2, A5, AFF_1:39;
then ( c,a // c,a' & c,b // c,b' ) by AFF_1:13;
then ( LIN c,a,a' & LIN c,b,b' ) by AFF_1:def 1;
then ( LIN a,a',c & LIN b,b',c ) by AFF_1:15;
then ( ( a = a' or c in Line o,a ) & ( b = b' or c in Line o,b ) ) by A7, A8, AFF_1:39;
hence contradiction by A2, A3, A5, A7, AFF_1:11, AFF_1:30; :: thesis: verum

end;