let AFP be AffinPlane; ( AFP is Moufangian implies for K, A, C being Subset of AFP
for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9 )
assume
AFP is Moufangian
; for K, A, C being Subset of AFP
for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9
then A1:
AFP is translational
by AFF_2:14;
let K, A, C be Subset of AFP; for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9
let p, q, a, a9, b, b9 be Element of AFP; ( K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 implies a,b // a9,b9 )
assume that
A2:
K // A
and
A3:
K // C
and
A4:
K <> A
and
A5:
K <> C
and
A6:
p in K
and
A7:
q in K
and
A8:
a in A
and
A9:
a9 in A
and
A10:
b in C
and
A11:
b9 in C
and
A12:
p,a // q,a9
and
A13:
p,b // q,b9
; a,b // a9,b9
A14:
A is being_line
by A2, AFF_1:36;
A15:
C is being_line
by A3, AFF_1:36;
K is being_line
by A2, AFF_1:36;
hence
a,b // a9,b9
by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A1, A14, A15, AFF_2:def 11; verum