let AP be AffinPlane; :: thesis: ( AP is Desarguesian implies AP is Moufangian )
assume A1: AP is Desarguesian ; :: thesis: AP is Moufangian
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:24;
A13: now :: thesis: not o = b
assume A14: o = b ; :: thesis: contradiction
b,a // K by A11, AFF_1:34;
hence contradiction by A2, A3, A5, A14, AFF_1:23; :: thesis: verum
end;
then A15: b in Line (o,b) by AFF_1:24;
A16: a in Line (o,a) by A3, A5, AFF_1:24;
A17: Line (o,a) is being_line by A3, A5, AFF_1:24;
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:40, AFF_1:41;
hence contradiction by A3, A5, A7, A11, A12, A16, AFF_1:45, AFF_1:53; :: thesis: verum
end;
A19: ( Line (o,b) is being_line & o in Line (o,b) ) by A13, AFF_1:24;
then A20: b9 in Line (o,b) by A9, A13, A15, AFF_1:25;
a9 in Line (o,a) by A3, A5, A8, A17, A12, A16, AFF_1:25;
hence b,c // b9,c9 by A1, A2, A3, A4, A5, A6, A10, A13, A17, A12, A16, A19, A15, A20, A18; :: thesis: verum