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, 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'

A3: now

assume o = b ; :: thesis: contradiction
then ( b in K & b,a // K ) by A2, AFF_1:48;
hence contradiction by A2, AFF_1:37; :: thesis: verum

end;

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

proof

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

end;

hence b,c // b',c' by A1, A2, A3, A4, A5, Def4; :: thesis: verum

end;