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 and
A2: not a in K and
A3: for x, y being Element of AFP holds
( f . x = y iff ( ( 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 ) ) ) ) ; :: thesis:
A4: K is being_line by A1, AFF_1:26;
A5: not b in K by A1, A2, AFF_1:35;
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 A6: A is being_line ; :: thesis:
set B9 = f .: A;

A7: now :: thesis:

assume that
A8: A // K and
A9: A <> K ; :: thesis:

now :: thesis:

let x be Element of AFP; :: thesis:
assume A10: x in A ; :: thesis:
consider y being Element of AFP such that
A11: f . y = x by TRANSGEO:1;
( ( 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,a // p9,y & p,b // p9,x & y,x // K ) ) ) by A3, A11;
then x,y // K by A8, A9, A10, AFF_1:34, AFF_1:45;
then x,y // A by A8, AFF_1:43;
then y in A by A6, A10, AFF_1:23;
hence x in f .: A by A11, TRANSGEO:91; :: thesis:

end;

then A12: A c= f .: A by SUBSET_1:2;

now :: thesis:

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 and
A14: y = f . x by TRANSGEO:91;
not x in K by A8, A9, A13, AFF_1:45;
then 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 ) by A3, A14;
then x,y // A by A8, AFF_1:43;
hence y in A by A6, A13, AFF_1:23; :: thesis:

end;

then f .: A c= A by SUBSET_1:2;
hence f .: A is being_line by A6, A12, XBOOLE_0:def 10; :: thesis:

end;

A15: now :: thesis:

K is being_line by A1, AFF_1:26;
then consider M being Subset of AFP such that
A16: a in M and
A17: K // M by AFF_1:49;
A18: M is being_line by A17, AFF_1:36;
consider A9 being Subset of AFP such that
A19: a in A9 and
A20: A // A9 by A6, AFF_1:49;
A21: A9 is being_line by A20, AFF_1:36;
assume that
A22: not A // K and
A23: A <> K ; :: thesis:
consider p being Element of AFP such that
A24: p in A and
A25: p in K by A4, A6, A22, AFF_1:58;
not A9 // K by A22, A20, AFF_1:44;
then consider q being Element of AFP such that
A26: q in A9 and
A27: q in K by A4, A21, AFF_1:58;
set C9 = Line (q,b);
A28: q in Line (q,b) by AFF_1:15;
a,b // M by A1, A17, AFF_1:43;
then b in M by A16, A18, AFF_1:23;
then q <> b by A2, A16, A17, A27, AFF_1:45;
then Line (q,b) is being_line by AFF_1:def 3;
then consider C being Subset of AFP such that
A29: p in C and
A30: Line (q,b) // C by AFF_1:49;
A31: b in Line (q,b) by AFF_1:15;
A32: C is being_line by A30, AFF_1:36;

now :: thesis:

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

A34: now :: thesis:

A35: q,b // p,y by A28, A31, A29, A30, A33, AFF_1:39;
K is being_line by A1, AFF_1:26;
then consider N being Subset of AFP such that
A36: y in N and
A37: K // N by AFF_1:49;
A38: N is being_line by A37, AFF_1:36;
not N // A by A22, A37, AFF_1:44;
then consider x being Element of AFP such that
A39: x in N and
A40: x in A by A6, A38, AFF_1:58;
A41: x,y // K by A36, A37, A39, AFF_1:40;
assume A42: y <> p ; :: thesis:
A43: not x in K

proof

assume x in K ; :: thesis:
then y in K by A36, A37, A39, AFF_1:45;
then Line (q,b) // K by A4, A25, A29, A30, A32, A33, A42, AFF_1:18;
hence contradiction by A5, A27, A28, A31, AFF_1:45; :: thesis:

end;

q,a // p,x by A24, A19, A20, A26, A40, AFF_1:39;
then y = f . x by A3, A25, A27, A43, A35, A41;
hence y in f .: A by A40, TRANSGEO:91; :: thesis:

end;

now :: thesis:

assume A44: y = p ; :: thesis:
f . p = p by A3, A25;
hence y in f .: A by A24, A44, TRANSGEO:91; :: thesis:

end;

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

end;

then A45: C c= f .: A by SUBSET_1:2;

now :: thesis:

let y be Element of AFP; :: thesis:
assume y in f .: A ; :: thesis:
then consider x being Element of AFP such that
A46: x in A and
A47: y = f . x by TRANSGEO:91;

now :: thesis:

K is being_line by A1, AFF_1:26;
then consider N being Subset of AFP such that
A48: x in N and
A49: K // N by AFF_1:49;
A50: not C // N

proof

assume C // N ; :: thesis:
then Line (q,b) // N by A30, AFF_1:44;
then A51: Line (q,b) // K by A49, AFF_1:44;
q in Line (q,b) by AFF_1:15;
then Line (q,b) = K by A27, A51, AFF_1:45;
hence contradiction by A5, AFF_1:15; :: thesis:

end;

N is being_line by A49, AFF_1:36;
then consider z being Element of AFP such that
A52: z in C and
A53: z in N by A32, A50, AFF_1:58;
A54: x,z // K by A48, A49, A53, AFF_1:40;
assume x <> p ; :: thesis:
then A55: not x in K by A4, A6, A23, A24, A25, A46, AFF_1:18;
A56: q,a // p,x by A24, A19, A20, A26, A46, AFF_1:39;
q,b // p,z by A28, A31, A29, A30, A52, AFF_1:39;
hence y in C by A3, A25, A27, A47, A55, A52, A56, A54; :: thesis:

end;

hence y in C by A3, A25, A29, A47; :: thesis:

end;

then f .: A c= C by SUBSET_1:2;
hence f .: A is being_line by A32, A45, XBOOLE_0:def 10; :: thesis:

end;

now :: thesis:

assume A57: A = K ; :: thesis:

now :: thesis:

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:91;
hence y in A by A3, A57; :: thesis:

end;

then A58: f .: A c= A by SUBSET_1:2;

now :: thesis:

let x be Element of AFP; :: thesis:
assume A59: x in A ; :: thesis:
set y = f . x;
f . x in f .: A by A59, TRANSGEO:90;
hence x in f .: A by A3, A57, A59; :: thesis:

end;

then A c= f .: A by SUBSET_1:2;
hence f .: A is being_line by A6, A58, XBOOLE_0:def 10; :: thesis:

end;

hence f .: A is being_line by A7, A15; :: thesis:

end;

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