let AFP be AffinPlane; :: thesis:
assume A1: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ; :: thesis:

now :: thesis:

let o be Element of AFP; :: thesis:
let K be Subset of AFP; :: thesis:
let c, c9, a, b, a9, b9 be Element of AFP; :: thesis:
assume that
A2: o in K and
A3: c in K and
A4: c9 in K and
A5: K is being_line and
A6: LIN o,a,a9 and
A7: LIN o,b,b9 and
A8: not a in K and
A9: a,b // K and
A10: a9,b9 // K and
A11: a,c // a9,c9 ; :: thesis:
consider f being Permutation of the carrier of AFP such that
A12: f is_Sc K and
A13: f . a = b by A1, A8, A9;
A14: f is collineation by A12;
A15: a,b // a9,b9 by A5, A9, A10, AFF_1:31;
A16: f . a9 = b9

proof

set x = f . a9;

A17: now :: thesis:

f . o = o by A2, A12;
then A18: LIN o,b,f . a9 by A6, A13, A14, TRANSGEO:88;
a9,f . a9 // K by A12;
then A19: a,b // a9,f . a9 by A5, A9, AFF_1:31;
assume a <> b ; :: thesis:
hence f . a9 = b9 by A2, A6, A7, A8, A9, A15, A19, A18, AFF_1:46, AFF_1:56; :: thesis:

end;

now :: thesis:

assume A20: a = b ; :: thesis:
then f = id the carrier of AFP by A8, A12, A13, Th5;
then f . a9 = a9 by FUNCT_1:18;
hence f . a9 = b9 by A2, A6, A7, A8, A10, A20, AFF_1:47; :: thesis:

end;

hence f . a9 = b9 by A17; :: thesis:

end;

A21: f . c9 = c9 by A4, A12;
f . c = c by A3, A12;
hence b,c // b9,c9 by A11, A13, A14, A21, A16, TRANSGEO:87; :: thesis:

end;

hence AFP is Moufangian by Lm2; :: thesis: