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