let AFP be AffinPlane; :: thesis:
let a, b be Element of AFP; :: thesis:
let K be Subset of AFP; :: thesis:
let f be Permutation of the carrier of AFP; :: thesis:
assume that
A1: ( a,b // K & not a in K ) and
AFP is Moufangian and
A2: for x, y being Element of AFP holds
( f . x = y iff ( ( 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 ) ) ) ) ; :: thesis:
A3: ( b,a // K & not b in K ) by A1, AFF_1:48, AFF_1:49;
A4: K is being_line by A1, AFF_1:40;
for A being Subset of AFP st A is being_line holds
f .: A is being_line

proof

let A be Subset of AFP; :: thesis:
assume A5: A is being_line ; :: thesis:
set B' = f .: A;

A6: now

assume A7: A = K ; :: thesis:
A8: A c= f .: A

proof

now

let x be Element of AFP; :: thesis:
assume A9: x in A ; :: thesis:
set y = f . x;
( f . x in f .: A & x = f . x ) by A2, A7, A9, TRANSGEO:110;
hence x in f .: A ; :: thesis:

end;

hence A c= f .: A by SUBSET_1:7; :: thesis:

end;

f .: A c= A

proof

now

let y be Element of AFP; :: thesis:
assume y in f .: A ; :: thesis:
then ex x being Element of AFP st
( x in A & y = f . x ) by TRANSGEO:111;
hence y in A by A2, A7; :: thesis:

end;

hence f .: A c= A by SUBSET_1:7; :: thesis:

end;

hence f .: A is being_line by A5, A8, XBOOLE_0:def 10; :: thesis:

end;

A10: now

assume A11: ( A // K & A <> K ) ; :: thesis:
A12: f .: A c= A

proof

now

let y be Element of AFP; :: thesis:
assume y in f .: A ; :: thesis:
then consider x being Element of AFP such that
A13: ( x in A & y = f . x ) by TRANSGEO:111;
not x in K by A11, A13, AFF_1:59;
then 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 ) by A2, A13;
then x,y // A by A11, AFF_1:57;
hence y in A by A5, A13, AFF_1:37; :: thesis:

end;

hence f .: A c= A by SUBSET_1:7; :: thesis:

end;

A c= f .: A

proof

now

let x be Element of AFP; :: thesis:
assume A14: x in A ; :: thesis:
consider y being Element of AFP such that
A15: f . y = x by TRANSGEO:2;
( ( 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,a // p',y & p,b // p',x & y,x // K ) ) ) by A2, A15;
then x,y // K by A11, A14, AFF_1:48, AFF_1:59;
then x,y // A by A11, AFF_1:57;
then y in A by A5, A14, AFF_1:37;
hence x in f .: A by A15, TRANSGEO:111; :: thesis:

end;

hence A c= f .: A by SUBSET_1:7; :: thesis:

end;

hence f .: A is being_line by A5, A12, XBOOLE_0:def 10; :: thesis:

end;

now

assume A16: ( not A // K & A <> K ) ; :: thesis:
then consider p being Element of AFP such that
A17: ( p in A & p in K ) by A4, A5, AFF_1:72;
consider M being Subset of AFP such that
A18: ( a in M & K // M ) by A4, AFF_1:63;
A19: M is being_line by A18, AFF_1:50;
A20: b in M

proof

a,b // M by A1, A18, AFF_1:57;
hence b in M by A18, A19, AFF_1:37; :: thesis:

end;

consider A' being Subset of AFP such that
A21: ( a in A' & A // A' ) by A5, AFF_1:63;
A22: A' is being_line by A21, AFF_1:50;
not A' // K by A16, A21, AFF_1:58;
then consider q being Element of AFP such that
A23: ( q in A' & q in K ) by A4, A22, AFF_1:72;
set C' = Line q,b;
q <> b by A1, A18, A20, A23, AFF_1:59;
then A24: ( Line q,b is being_line & q in Line q,b & b in Line q,b ) by AFF_1:26, AFF_1:def 3;
then consider C being Subset of AFP such that
A25: ( p in C & Line q,b // C ) by AFF_1:63;
A26: C is being_line by A25, AFF_1:50;
A27: C c= f .: A

proof

now

let y be Element of AFP; :: thesis:
assume A28: y in C ; :: thesis:

A29: now

assume A30: y = p ; :: thesis:
f . p = p by A2, A17;
hence y in f .: A by A17, A30, TRANSGEO:111; :: thesis:

end;

now

assume A31: y <> p ; :: thesis:
consider N being Subset of AFP such that
A32: ( y in N & K // N ) by A4, AFF_1:63;
A33: ( N is being_line & N // K ) by A32, AFF_1:50;
not N // A by A16, A32, AFF_1:58;
then consider x being Element of AFP such that
A34: ( x in N & x in A ) by A5, A33, AFF_1:72;
A35: not x in K

proof

assume x in K ; :: thesis:
then y in K by A32, A34, AFF_1:59;
then Line q,b // K by A4, A17, A25, A26, A28, A31, AFF_1:30;
hence contradiction by A3, A23, A24, AFF_1:59; :: thesis:

end;

( q,a // p,x & q,b // p,y & x,y // K ) by A17, A21, A23, A24, A25, A28, A32, A34, AFF_1:53, AFF_1:54;
then y = f . x by A2, A17, A23, A35;
hence y in f .: A by A34, TRANSGEO:111; :: thesis:

end;

hence y in f .: A by A29; :: thesis:

end;

hence C c= f .: A by SUBSET_1:7; :: thesis:

end;

f .: A c= C

proof

now

let y be Element of AFP; :: thesis:
assume y in f .: A ; :: thesis:
then consider x being Element of AFP such that
A36: ( x in A & y = f . x ) by TRANSGEO:111;

now

assume A37: x <> p ; :: thesis:
consider N being Subset of AFP such that
A38: ( x in N & K // N ) by A4, AFF_1:63;
A39: ( N is being_line & N // K ) by A38, AFF_1:50;
A40: not x in K by A4, A5, A16, A17, A36, A37, AFF_1:30;
not C // N

proof

assume C // N ; :: thesis:
then ( Line q,b // N & N // K ) by A25, A38, AFF_1:58;
then ( Line q,b // K & q in Line q,b ) by AFF_1:26, AFF_1:58;
then Line q,b = K by A23, AFF_1:59;
hence contradiction by A3, AFF_1:26; :: thesis:

end;

then consider z being Element of AFP such that
A41: ( z in C & z in N ) by A26, A39, AFF_1:72;
( q,a // p,x & q,b // p,z & x,z // K ) by A17, A21, A23, A24, A25, A36, A38, A41, AFF_1:53, AFF_1:54;
hence y in C by A2, A17, A23, A36, A40, A41; :: thesis:

end;

hence y in C by A2, A17, A25, A36; :: thesis:

end;

hence f .: A c= C by SUBSET_1:7; :: thesis:

end;

hence f .: A is being_line by A26, A27, XBOOLE_0:def 10; :: thesis:

end;

hence f .: A is being_line by A6, A10; :: thesis:

end;

hence f is collineation by TRANSGEO:116; :: thesis: