let AFP be AffinPlane; :: thesis: ( ( 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 ) ) implies AFP is Moufangian )
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: AFP is Moufangian

now :: thesis: for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9

let o be Element of AFP; :: thesis: for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let K be Subset of AFP; :: thesis: for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let c, c9, a, b, a9, b9 be Element of AFP; :: thesis: ( o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 implies b,c // b9,c9 )
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: b,c // b9,c9
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: ( a <> b implies f . a9 = b9 )

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: f . a9 = b9
hence f . a9 = b9 by A2, A6, A7, A8, A9, A15, A19, A18, AFF_1:46, AFF_1:56; :: thesis: verum

end;

now :: thesis: ( a = b implies f . a9 = b9 )

assume A20: a = b ; :: thesis: f . a9 = b9
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: verum

end;

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

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: verum

end;

hence AFP is Moufangian by Lm2; :: thesis: verum