let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds
for F being IncProjMap of G_ k,X, G_ k,X holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s )
let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for F being IncProjMap of G_ k,X, G_ k,X holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s ) )
assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis: for F being IncProjMap of G_ k,X, G_ k,X holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s )
let F be IncProjMap of G_ k,X, G_ k,X; :: thesis: ( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s )
A2: ( F is automorphism implies ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s )

proof

assume A3: F is automorphism ; :: thesis: ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
A4: ( 0 + 1 < k + 1 & succ k = k + 1 & card 1 = 1 & card (k + 1) = k + 1 & card k = k ) by A1, CARD_1:def 5, NAT_1:39, XREAL_1:10;
then ( 1 in succ k & k + 1 in succ (card X) ) by A1, NAT_1:42, ORDINAL1:34;
then ( ( 1 = k or 1 in k ) & ( k + 1 = card X or k + 1 in card X ) & succ 1 = 1 + 1 & succ (k + 1) = (k + 1) + 1 ) by NAT_1:39, ORDINAL1:13;
then ( ( 1 = k or ( 1 < k & 2 c= k ) ) & ( k + 1 = card X or k + 2 c= card X ) ) by A4, NAT_1:42, ORDINAL1:33;
then ( 1 = k or ( 1 < k & card X = k + 1 ) or ( 2 <= k & k + 2 c= card X ) ) by NAT_1:40;
hence ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s by A1, A3, Th24, Th25, Th33; :: thesis: verum

end;

( ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s implies F is automorphism )

proof

assume ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s ; :: thesis: F is automorphism
then consider s being Permutation of X such that
A5: IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s ;
incprojmap k,s is automorphism by A1, Th34;
then A6: ( the line-map of F is bijective & the point-map of F is bijective & incprojmap k,s is incidence_preserving ) by A5, Def9;
F is incidence_preserving

proof

let A be POINT of (G_ k,X); :: according to COMBGRAS:def 8 :: thesis: for L1 being LINE of (G_ k,X) holds
( A on L1 iff F . A on F . L1 )
let L be LINE of (G_ k,X); :: thesis: ( A on L iff F . A on F . L )
( F . A = (incprojmap k,s) . A & F . L = (incprojmap k,s) . L ) by A5;
hence ( A on L iff F . A on F . L ) by A6, Def8; :: thesis: verum

end;

hence F is automorphism by A6, Def9; :: thesis: verum

end;

hence ( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s ) by A2; :: thesis: verum