let AFP be AffinPlane; for a, b, p, p9, q, q9, s, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds
s = y
let a, b, p, p9, q, q9, s, x, y be Element of AFP; for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds
s = y
let K be Subset of AFP; ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s implies s = y )
assume that
A1:
a,b // K
and
A2:
not a in K
and
A3:
not x in K
and
A4:
AFP is Moufangian
and
A5:
p in K
and
A6:
p9 in K
and
A7:
p,a // p9,x
and
A8:
p,b // p9,y
and
A9:
x,y // K
and
A10:
q in K
and
A11:
q9 in K
and
A12:
q,a // q9,x
and
A13:
x,s // K
and
A14:
q,b // q9,s
; s = y
A15:
not b in K
by A1, A2, AFF_1:35;
q,b // q9,y
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, Lm21;
then
q9,s // q9,y
by A10, A14, A15, AFF_1:5;
then
LIN q9,s,y
by AFF_1:def 1;
then A16:
LIN y,s,q9
by AFF_1:6;
assume A17:
not s = y
; contradiction
K is being_line
by A1, AFF_1:26;
then consider M being Subset of AFP such that
A18:
x in M
and
A19:
K // M
by AFF_1:49;
A20:
M is being_line
by A19, AFF_1:36;
x,s // M
by A13, A19, AFF_1:43;
then A21:
s in M
by A18, A20, AFF_1:23;
x,y // M
by A9, A19, AFF_1:43;
then
y in M
by A18, A20, AFF_1:23;
then
M = Line (y,s)
by A17, A20, A21, AFF_1:24;
then
q9 in M
by A16, AFF_1:def 2;
hence
contradiction
by A3, A11, A18, A19, AFF_1:45; verum