let AP be AffinPlane; :: thesis: ( AP is satisfying_TDES_3 implies AP is Moufangian )
assume A1: AP is satisfying_TDES_3 ; :: thesis: AP is Moufangian
thus AP is Moufangian :: thesis: verum

proof

let K be Subset of AP; :: according to AFF_2:def 7 :: 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' & a,b // a',b' & a,c // a',c' & a,b // K holds
b,c // b',c'
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' & a,b // a',b' & a,c // a',c' & a,b // K implies b,c // b',c' )
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' & a,b // a',b' & a,c // a',c' & a,b // K ) ; :: thesis: b,c // b',c'
assume A3: not b,c // b',c' ; :: thesis: contradiction
then A4: ( b <> c & b' <> c' ) by AFF_1:12;
A5: ( o <> a & o <> b & a <> c & b <> c ) by A2, AFF_1:49;
A6: not LIN a,b,c

proof

assume LIN a,b,c ; :: thesis: contradiction
then a,b // a,c by AFF_1:def 1;
then a,c // K by A2, AFF_1:46;
then c,a // K by AFF_1:48;
hence contradiction by A2, AFF_1:37; :: thesis: verum

end;

set A = Line o,a;
set P = Line o,b;
set M = Line b,c;
set T = Line a',c';
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 A5, AFF_1:38;
then A8: ( a' in Line o,a & b' in Line o,b ) by A2, A5, AFF_1:39;
A9: Line o,a <> Line o,b

proof

assume Line o,a = Line o,b ; :: thesis: contradiction
then a,b // Line o,a by A7, AFF_1:54, AFF_1:55;
hence contradiction by A2, A7, AFF_1:59, AFF_1:67; :: thesis: verum

end;

A10: a' <> b'

proof

assume A11: a' = b' ; :: thesis: contradiction
then ( a' in K & a',c' // c,a ) by A2, A7, A8, A9, AFF_1:13, AFF_1:30;
then a' = c' by A2, AFF_1:62;
hence contradiction by A3, A11, AFF_1:12; :: thesis: verum

end;

A12: a' <> c'

proof

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

end;

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

proof

assume a',c' // N ; :: thesis: contradiction
then ( a',c' // N & a',c' // a,c ) by A2, AFF_1:13;
then a,c // N by A12, AFF_1:46;
then a,c // Line b,c by A14, AFF_1:57;
then c,a // Line b,c by AFF_1:48;
then a in Line b,c by A13, AFF_1:37;
hence contradiction by A6, A13, AFF_1:33; :: thesis: verum

end;

then consider x being Element of AP such that
A16: ( x in N & LIN a',c',x ) by A15, AFF_1:73;
A17: x in Line a',c' by A12, A13, A16, AFF_1:39;
A18: b,c // b',x by A13, A14, A16, AFF_1:53;
a,c // a',x

proof

a',c' // a',x by A16, AFF_1:def 1;
hence a,c // a',x by A2, A12, AFF_1:14; :: thesis: verum

end;

then x in K by A1, A2, A18, Def10;
then K = Line a',c' by A2, A3, A13, A17, A18, AFF_1:30;
then ( a' in Line o,b & a',b' // b,a ) by A2, A7, A8, A13, AFF_1:13, AFF_1:30;
then a in Line o,b by A7, A8, A10, AFF_1:62;
hence contradiction by A2, A7, A9, AFF_1:30; :: thesis: verum

end;