let AFP be AffinPlane; :: thesis: for a, b, x, p, p', y, q, q', s being Element of
for K being Subset of st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x & x,s // K & q,b // q',s holds
s = y
let a, b, x, p, p', y, q, q', s be Element of ; :: thesis: for K being Subset of st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x & x,s // K & q,b // q',s holds
s = y
let K be Subset of ; :: thesis: ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x & x,s // K & q,b // q',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: p' in K and
A7: p,a // p',x and
A8: p,b // p',y and
A9: x,y // K and
A10: q in K and
A11: q' in K and
A12: q,a // q',x and
A13: x,s // K and
A14: q,b // q',s ; :: thesis: s = y
A15: not b in K by A1, A2, AFF_1:49;
q,b // q',y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, Lm21;
then q',s // q',y by A10, A14, A15, AFF_1:14;
then LIN q',s,y by AFF_1:def 1;
then A16: LIN y,s,q' by AFF_1:15;
assume A17: not s = y ; :: thesis: contradiction
consider M being Subset of such that
A18: x in M and
A19: K // M by A1, AFF_1:40, AFF_1:63;
A20: M is being_line by A19, AFF_1:50;
x,s // M by A13, A19, AFF_1:57;
then A21: s in M by A18, A20, AFF_1:37;
x,y // M by A9, A19, AFF_1:57;
then y in M by A18, A20, AFF_1:37;
then M = Line y,s by A17, A20, A21, AFF_1:38;
then q' in M by A16, AFF_1:def 2;
hence contradiction by A3, A11, A18, A19, AFF_1:59; :: thesis: verum