let AFP be AffinPlane; :: thesis: ( ( for a, b being Element of
for K being Subset of 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
for K being Subset of 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

let o be Element of ; :: thesis: for K being Subset of
for c, c', a, b, a', b' being Element of st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c'
let K be Subset of ; :: thesis: for c, c', a, b, a', b' being Element of st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c'
let c, c', a, b, a', b' be Element of ; :: thesis: ( o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' implies b,c // b',c' )
assume that
A2: o in K and
A3: c in K and
A4: c' in K and
A5: K is being_line and
A6: LIN o,a,a' and
A7: LIN o,b,b' and
A8: not a in K and
A9: a,b // K and
A10: a',b' // K and
A11: a,c // a',c' ; :: thesis: b,c // b',c'
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, Def1;
A15: a,b // a',b' by A5, A9, A10, AFF_1:45;
A16: f . a' = b'

proof

set x = f . a';

A17: now

f . o = o by A2, A12, Def1;
then A18: LIN o,b,f . a' by A6, A13, A14, TRANSGEO:108;
a',f . a' // K by A12, Def1;
then A19: a,b // a',f . a' by A5, A9, AFF_1:45;
assume a <> b ; :: thesis: f . a' = b'
hence f . a' = b' by A2, A6, A7, A8, A9, A15, A19, A18, AFF_1:60, AFF_1:70; :: thesis: verum

end;

now

assume A20: a = b ; :: thesis: f . a' = b'
then f = id the carrier of AFP by A8, A12, A13, Th5;
then f . a' = a' by FUNCT_1:35;
hence f . a' = b' by A2, A6, A7, A8, A10, A20, AFF_1:61; :: thesis: verum

end;

hence f . a' = b' by A17; :: thesis: verum

end;

A21: f . c' = c' by A4, A12, Def1;
f . c = c by A3, A12, Def1;
hence b,c // b',c' by A11, A13, A14, A21, A16, TRANSGEO:107; :: thesis: verum

end;

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