theorem Th7:
for
AFP being
AffinPlane for
a,
b,
p,
p9,
q,
q9,
x,
y being
Element of
AFP for
M,
K being
Subset of
AFP st
K // M &
p in K &
q in K &
p9 in K &
q9 in K &
AFP is
Moufangian &
a in M &
b in M &
x in M &
y in M &
a <> b &
q <> p &
p,
a // p9,
x &
p,
b // p9,
y &
q,
a // q9,
x holds
q,
b // q9,
y