let AFP be AffinPlane; :: thesis: for a, b, x, y, r being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',r & p,b // p',y & r,y // K ) ) ) holds
x = r
let a, b, x, y, r be Element of AFP; :: thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',r & p,b // p',y & r,y // K ) ) ) holds
x = r
let K be Subset of AFP; :: thesis: ( a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',r & p,b // p',y & r,y // K ) ) ) implies x = r )
assume that
A1: ( a,b // K & not a in K & AFP is Moufangian ) and
A2: ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) and
A3: ( ( r in K & r = y ) or ( not r in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',r & p,b // p',y & r,y // K ) ) ) ; :: thesis: x = r
A4: ( b,a // K & not b in K ) by A1, AFF_1:48, AFF_1:49;
A5: ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) by A1, A2, Lm18;
( ( y in K & y = r ) or ( not y in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,b // p',y & p,a // p',r & y,r // K ) ) ) by A1, A3, Lm18;
hence x = r by A1, A4, A5, Lm22; :: thesis: verum