let AFP be AffinPlane; for a, b, r, x, y 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, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds
x = r
let a, b, r, x, y be 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, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds
x = r
let K be Subset of AFP; ( a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) implies x = r )
assume that
A1:
a,b // K
and
A2:
not a in K
and
A3:
AFP is Moufangian
and
A4:
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
and
A5:
( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) )
; x = r
A6:
( ( y in K & y = r ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,r & y,r // K ) ) )
by A1, A2, A5, Lm18;
A7:
b,a // K
by A1, AFF_1:34;
A8:
not b in K
by A1, A2, AFF_1:35;
( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) )
by A1, A2, A4, Lm18;
hence
x = r
by A3, A7, A8, A6, Lm22; verum