let AS be AffinSpace; ( AS is Desarguesian implies AS is Moufangian )
assume A1:
AS is Desarguesian
; AS is Moufangian
now 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,c9let K be
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,c9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AS;
( 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
;
b,c // b9,c9set A =
Line (
o,
a);
set P =
Line (
o,
b);
A12:
o in Line (
o,
a)
by A3, A5, AFF_1:24;
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)
;
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;
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, AFF_2:def 4;
verum end;
hence
AS is Moufangian
by AFF_2:def 7; verum