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, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: o <> c and
A8: a <> b and
A9: LIN o,a,a9 and
A10: LIN o,b,b9 and
A11: a,b // a9,b9 and
A12: a,c // a9,c9 and
A13: a,b // K ; :: thesis: b,c // b9,c9
set A = Line o,a;
set P = Line o,b;
set M = Line b,c;
set T = Line a9,c9;
A14: o in Line o,a by A3, A6, AFF_1:38;
assume A15: not b,c // b9,c9 ; :: thesis: contradiction
then A16: b <> c by AFF_1:12;
then A17: b in Line b,c by AFF_1:38;
A18: a9,b9 // b,a by A11, AFF_1:13;
A19: c in Line b,c by A16, AFF_1:38;
A20: a in Line o,a by A3, A6, AFF_1:38;
A21: Line o,a is being_line by A3, A6, AFF_1:38;
then A22: a9 in Line o,a by A3, A6, A9, A14, A20, AFF_1:39;
A23: o <> b by A3, A6, A13, AFF_1:49;
then A24: Line o,b is being_line by AFF_1:38;
A25: b in Line o,b by A23, AFF_1:38;
A26: Line o,a <> Line o,b

proof

assume Line o,a = Line o,b ; :: thesis: contradiction
then a,b // Line o,a by A21, A20, A25, AFF_1:54, AFF_1:55;
hence contradiction by A3, A6, A8, A13, A14, A20, AFF_1:59, AFF_1:67; :: thesis: verum

end;

A27: o in Line o,b by A23, AFF_1:38;
then A28: b9 in Line o,b by A10, A23, A24, A25, AFF_1:39;
A29: a9 <> b9

proof

A30: a9,c9 // c,a by A12, AFF_1:13;
assume A31: a9 = b9 ; :: thesis: contradiction
then a9 in K by A3, A21, A24, A14, A27, A22, A28, A26, AFF_1:30;
then a9 = c9 by A2, A4, A5, A6, A30, AFF_1:62;
hence contradiction by A15, A31, AFF_1:12; :: thesis: verum

end;

A32: a9 <> c9

proof

assume a9 = c9 ; :: thesis: contradiction
then A33: a9 in Line o,b by A2, A3, A5, A6, A21, A14, A20, A27, A22, AFF_1:30;
a9,b9 // b,a by A11, AFF_1:13;
then a in Line o,b by A24, A25, A28, A29, A33, AFF_1:62;
hence contradiction by A3, A6, A24, A27, A26, AFF_1:38; :: thesis: verum

end;

then A34: ( Line a9,c9 is being_line & c9 in Line a9,c9 ) by AFF_1:38;
A35: Line b,c is being_line by A16, AFF_1:38;
then consider N being Subset of AP such that
A36: b9 in N and
A37: Line b,c // N by AFF_1:63;
A38: N is being_line by A37, AFF_1:50;
A39: 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 A8, A13, AFF_1:46;
then c,a // K by AFF_1:48;
hence contradiction by A2, A4, A6, AFF_1:37; :: thesis: verum

end;

not a9,c9 // N

proof

assume A40: a9,c9 // N ; :: thesis: contradiction
a9,c9 // a,c by A12, AFF_1:13;
then a,c // N by A32, A40, AFF_1:46;
then a,c // Line b,c by A37, AFF_1:57;
then c,a // Line b,c by AFF_1:48;
then a in Line b,c by A35, A19, AFF_1:37;
hence contradiction by A39, A35, A17, A19, AFF_1:33; :: thesis: verum

end;

then consider x being Element of AP such that
A41: x in N and
A42: LIN a9,c9,x by A38, AFF_1:73;
A43: b,c // b9,x by A17, A19, A36, A37, A41, AFF_1:53;
a9,c9 // a9,x by A42, AFF_1:def 1;
then a,c // a9,x by A12, A32, AFF_1:14;
then A44: x in K by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A13, A43, Def10;
A45: a9 in Line a9,c9 by A32, AFF_1:38;
then x in Line a9,c9 by A32, A34, A42, AFF_1:39;
then K = Line a9,c9 by A2, A5, A15, A34, A43, A44, AFF_1:30;
then a9 in Line o,b by A2, A3, A6, A21, A14, A20, A27, A22, A45, AFF_1:30;
then a in Line o,b by A24, A25, A28, A29, A18, AFF_1:62;
hence contradiction by A3, A6, A24, A27, A26, AFF_1:38; :: thesis: verum

end;