let AS be AffinSpace; :: thesis: ( AS is Desarguesian implies AS is Moufangian )

assume A1: AS is Desarguesian ; :: thesis: AS is Moufangian

assume A1: AS is Desarguesian ; :: thesis: AS is Moufangian

now :: thesis: for K being Subset of AS

for o, a, b, c, a9, b9, c9 being Element of AS 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

hence
AS is Moufangian
by AFF_2:def 7; :: thesis: verumfor o, a, b, c, a9, b9, c9 being Element of AS 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 K be Subset of AS; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AS 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 AS; :: 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;

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)

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, AFF_2:def 4; :: thesis: verum

end;b,c // b9,c9

let o, a, b, c, a9, b9, c9 be Element of AS; :: 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

then A15:
b in Line (o,b)
by AFF_1:24;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;b,a // K by A11, AFF_1:34;

hence contradiction by A2, A3, A5, A14, AFF_1:23; :: thesis: verum

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

A19:
( Line (o,b) is being_line & o in Line (o,b) )
by A13, AFF_1:24;
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;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

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, AFF_2:def 4; :: thesis: verum