let AP be AffinPlane; :: thesis: ( AP is Desarguesian implies AP is Moufangian )
assume A1: AP is Desarguesian ; :: 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 & c9 in K ) and
A5: not a in K and
A6: o <> c and
A7: a <> b and
A8: LIN o,a,a9 and
A9: LIN o,b,b9 and
A10: ( a,b // a9,b9 & a,c // a9,c9 ) and
A11: a,b // K ; :: thesis: b,c // b9,c9
set A = Line o,a;
set P = Line o,b;
A12: o in Line o,a by A3, A5, AFF_1:38;

A13: now

assume A14: o = b ; :: thesis: contradiction
b,a // K by A11, AFF_1:48;
hence contradiction by A2, A3, A5, A14, AFF_1:37; :: thesis: verum

end;

then A15: b in Line o,b by AFF_1:38;
A16: a in Line o,a by A3, A5, AFF_1:38;
A17: Line o,a is being_line by A3, A5, AFF_1:38;
A18: Line o,a <> Line o,b

proof

assume Line o,a = Line o,b ; :: thesis: contradiction
then a,b // Line o,a by A17, A16, A15, AFF_1:54, AFF_1:55;
hence contradiction by A3, A5, A7, A11, A12, A16, AFF_1:59, AFF_1:67; :: thesis: verum

end;

A19: ( Line o,b is being_line & o in Line o,b ) by A13, AFF_1:38;
then A20: b9 in Line o,b by A9, A13, A15, AFF_1:39;
a9 in Line o,a by A3, A5, A8, A17, A12, A16, AFF_1:39;
hence b,c // b9,c9 by A1, A2, A3, A4, A5, A6, A10, A13, A17, A12, A16, A19, A15, A20, A18, Def4; :: thesis: verum

end;