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

proof

let A be Subset of AP; :: according to AFF_2:def 12 :: thesis: for P, C being Subset of AP
for a, b, c, a', b', c' being Element of AP st A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
A // C
let P, C be Subset of AP; :: thesis: for a, b, c, a', b', c' being Element of AP st A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
A // C
let a, b, c, a', b', c' be Element of AP; :: thesis: ( A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' implies A // C )
assume A2: ( A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' ) ; :: thesis: A // C
assume A3: not A // C ; :: thesis: contradiction
then consider o being Element of AP such that
A4: ( o in A & o in C ) by A2, AFF_1:72;
consider M being Subset of AP such that
A5: ( c in M & A // M ) by A2, AFF_1:63;
consider N being Subset of AP such that
A6: ( c' in N & A // N ) by A2, AFF_1:63;
A7: ( M is being_line & N is being_line & M // A & N // A ) by A5, A6, AFF_1:50;
A8: ( M // N & N // M & M // P & N // P ) by A2, A5, A6, AFF_1:58;
A9: ( a <> b & b <> c & a <> c ) by A2, AFF_1:16;
A10: ( a <> b' & a' <> b & a' <> b' ) by A2, AFF_1:59;
A11: a <> a'

proof

assume A12: a = a' ; :: thesis: contradiction
then LIN a,b,b' by A2, AFF_1:def 1;
then LIN b,b',a by AFF_1:15;
then ( b = b' or a in P ) by A2, AFF_1:39;
then ( LIN b,c,c' & LIN a,c,c' ) by A2, A12, AFF_1:59, AFF_1:def 1;
then ( LIN c,c',a & LIN c,c',b & LIN c,c',c ) by AFF_1:15, AFF_1:16;
hence contradiction by A2, AFF_1:17; :: thesis: verum

end;

A13: b <> b'

proof

assume b = b' ; :: thesis: contradiction
then b,a // b,a' by A2, 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 A2, A11, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

A14: a' <> c'

proof

assume a' = c' ; :: thesis: contradiction
then b,c // a',b' by A2, AFF_1:13;
then a,b // b,c by A2, A10, 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 A2, AFF_1:15; :: thesis: verum

end;

set P' = Line a,b;
set C' = Line a',b';
A15: ( Line a,b is being_line & Line a',b' is being_line & b in Line a,b & a in Line a,b & b' in Line a',b' & a' in Line a',b' ) by A9, A10, AFF_1:38;
A16: Line a,b // Line a',b' by A2, A9, A10, AFF_1:51;
not M // Line a,b

proof

assume M // Line a,b ; :: thesis: contradiction
then A // Line a,b by A5, AFF_1:58;
then b in A by A2, A15, AFF_1:59;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

then consider p being Element of AP such that
A17: ( p in M & p in Line a,b ) by A7, A15, AFF_1:72;
not N // Line a',b'

proof

assume N // Line a',b' ; :: thesis: contradiction
then A // Line a',b' by A6, AFF_1:58;
then b' in A by A2, A15, AFF_1:59;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

then consider q being Element of AP such that
A18: ( q in N & q in Line a',b' ) by A7, A15, AFF_1:72;
not P // C by A2, A3, AFF_1:58;
then consider s being Element of AP such that
A19: ( s in P & s in C ) by A2, AFF_1:72;
A20: LIN s,c,c' by A2, A19, AFF_1:33;
A21: c <> p by A2, A15, A17, AFF_1:33;
A22: c,p // P by A5, A8, A17, AFF_1:54;
A23: p,b // q,b' by A15, A16, A17, A18, AFF_1:53;
A24: not c in P

proof

assume c in P ; :: thesis: contradiction
then ( c in P & c' in P ) by A2, A9, AFF_1:62;
hence contradiction by A2, A3, AFF_1:30; :: thesis: verum

end;

A25: s <> b

proof

assume s = b ; :: thesis: contradiction
then ( b in C & b,c // c',b' ) by A2, A19, AFF_1:13;
then ( b in C & b' in C ) by A2, A9, AFF_1:62;
hence contradiction by A2, A3, A13, AFF_1:30; :: thesis: verum

end;

A26: c,p // c',q by A5, A6, A8, A17, A18, AFF_1:53;
c,b // c',b' by A2, AFF_1:13;
then A27: LIN s,p,q by A1, A2, A19, A20, A21, A22, A23, A24, A25, A26, Def8;
A28: LIN o,c',c by A2, A4, AFF_1:33;
A29: not c' in A

proof

assume c' in A ; :: thesis: contradiction
then ( c' in A & a',c' // a,c ) by A2, AFF_1:13;
then ( c in A & c' in A ) by A2, A14, AFF_1:62;
hence contradiction by A2, AFF_1:30; :: thesis: verum

end;

A30: c',q // c,p by A5, A6, A8, A17, A18, AFF_1:53;
A31: c',a' // c,a by A2, AFF_1:13;
A32: q,a' // p,a by A15, A16, A17, A18, AFF_1:53;
A33: c',q // A by A6, A18, AFF_1:54;
A34: c' <> q

proof

assume c' = q ; :: thesis: contradiction
then LIN a',b',c' by A15, A18, AFF_1:33;
then a',b' // a',c' by AFF_1:def 1;
then a',b' // a,c by A2, A14, AFF_1:14;
then a,b // a,c by A2, A10, AFF_1:14;
hence contradiction by A2, AFF_1:def 1; :: thesis: verum

end;

o <> a'

proof

assume o = a' ; :: thesis: contradiction
then ( a' in C & a',c' // c,a ) by A2, A4, AFF_1:13;
then ( a in C & a' in C ) by A2, A14, AFF_1:62;
hence contradiction by A2, A11, AFF_1:30; :: thesis: verum

end;

then LIN o,q,p by A1, A2, A4, A28, A29, A30, A31, A32, A33, A34, Def8;
then A35: ( LIN p,q,o & LIN p,q,s & LIN p,q,p ) by A27, AFF_1:15, AFF_1:16;

now

assume p = q ; :: thesis: contradiction
then M = N by A8, A17, A18, AFF_1:59;
hence contradiction by A2, A3, A5, A6, A7, AFF_1:30; :: thesis: verum

end;

then ( o = s or p in C ) by A2, A4, A19, A35, AFF_1:17, AFF_1:39;
then c in Line a,b by A2, A3, A4, A5, A7, A17, A19, AFF_1:30, AFF_1:59;
hence contradiction by A2, A15, AFF_1:33; :: thesis: verum

end;