let k be Nat; :: thesis: for X being non empty set st 0 < k & k + 3 c= card X holds
for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F holds
for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)

let X be non empty set ; :: thesis: ( 0 < k & k + 3 c= card X implies for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F holds
for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f) )

assume that
A1: 0 < k and
A2: k + 3 c= card X ; :: thesis: for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F holds
for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)

k + 1 <= k + 3 by XREAL_1:7;
then Segm (k + 1) c= Segm (k + 3) by NAT_1:39;
then A3: k + 1 c= card X by A2;
then A4: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by ;
k + 2 <= k + 3 by XREAL_1:7;
then Segm (k + 2) c= Segm (k + 3) by NAT_1:39;
then A5: (k + 1) + 1 c= card X by A2;
then A6: the Points of (G_ ((k + 1),X)) = { A where A is Subset of X : card A = k + 1 } by Def1;
k + 0 <= k + 1 by XREAL_1:7;
then A7: Segm k c= Segm (k + 1) by NAT_1:39;
k + 1 <= k + 2 by XREAL_1:7;
then A8: Segm (k + 1) c= Segm (k + 2) by NAT_1:39;
let F be IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X); :: thesis: ( F is automorphism implies for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F holds
for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f) )

assume A9: F is automorphism ; :: thesis: for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F holds
for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)

A10: F is incidence_preserving by A9;
let H be IncProjMap over G_ (k,X), G_ (k,X); :: thesis: ( the line-map of H = the point-map of F implies for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f) )

assume A11: the line-map of H = the point-map of F ; :: thesis: for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)

A12: dom the point-map of F = the Points of (G_ ((k + 1),X)) by FUNCT_2:52;
let f be Permutation of X; :: thesis: ( IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) implies IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f) )
assume A13: IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) ; :: thesis: IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)
A14: for x being object st x in dom the point-map of F holds
the point-map of F . x = the point-map of (incprojmap ((k + 1),f)) . x
proof
let x be object ; :: thesis: ( x in dom the point-map of F implies the point-map of F . x = the point-map of (incprojmap ((k + 1),f)) . x )
assume x in dom the point-map of F ; :: thesis: the point-map of F . x = the point-map of (incprojmap ((k + 1),f)) . x
then consider A being POINT of (G_ ((k + 1),X)) such that
A15: x = A ;
consider A1 being LINE of (G_ (k,X)) such that
A16: x = A1 by A4, A6, A15;
(incprojmap (k,f)) . A1 = f .: A1 by ;
then F . A = (incprojmap ((k + 1),f)) . A by A11, A13, A5, A15, A16, Def14;
hence the point-map of F . x = the point-map of (incprojmap ((k + 1),f)) . x by A15; :: thesis: verum
end;
A17: the Lines of (G_ ((k + 1),X)) = { L where L is Subset of X : card L = (k + 1) + 1 } by ;
A18: the point-map of F is bijective by A9;
A19: for x being object st x in dom the line-map of F holds
the line-map of F . x = the line-map of (incprojmap ((k + 1),f)) . x
proof
let x be object ; :: thesis: ( x in dom the line-map of F implies the line-map of F . x = the line-map of (incprojmap ((k + 1),f)) . x )
assume x in dom the line-map of F ; :: thesis: the line-map of F . x = the line-map of (incprojmap ((k + 1),f)) . x
then consider A being LINE of (G_ ((k + 1),X)) such that
A20: x = A ;
reconsider x = x as set by TARSKI:1;
x in the Lines of (G_ ((k + 1),X)) by A20;
then A21: ex A11 being Subset of X st
( x = A11 & card A11 = (k + 1) + 1 ) by A17;
then consider B1 being set such that
A22: B1 c= x and
A23: card B1 = k + 1 by ;
A24: x is finite by A21;
then A25: card (x \ B1) = (k + 2) - (k + 1) by ;
B1 c= X by ;
then B1 in the Points of (G_ ((k + 1),X)) by ;
then consider b1 being POINT of (G_ ((k + 1),X)) such that
A26: b1 = B1 ;
consider C1 being set such that
A27: C1 c= B1 and
A28: card C1 = k by ;
B1 is finite by A23;
then A29: card (C1 \/ (x \ B1)) = k + 1 by ;
C1 c= x by ;
then A30: C1 \/ (x \ B1) c= x by XBOOLE_1:8;
then C1 \/ (x \ B1) c= X by ;
then C1 \/ (x \ B1) in the Points of (G_ ((k + 1),X)) by ;
then consider b2 being POINT of (G_ ((k + 1),X)) such that
A31: b2 = C1 \/ (x \ B1) ;
b2 on A by A5, A20, A30, A31, Th10;
then F . b2 on F . A by A10;
then A32: F . b2 c= F . A by ;
B1 \/ (C1 \/ (x \ B1)) c= x by ;
then A33: card (b1 \/ b2) c= k + 2 by ;
B1 misses x \ B1 by XBOOLE_1:79;
then card ((x \ B1) /\ B1) = 0 by ;
then A34: b1 <> b2 by ;
then (k + 1) + 1 c= card (b1 \/ b2) by A23, A29, A26, A31, Th1;
then card (b1 \/ b2) = k + 2 by ;
then A35: b1 \/ b2 = x by ;
F . b2 in the Points of (G_ ((k + 1),X)) ;
then A36: ex B12 being Subset of X st
( F . b2 = B12 & card B12 = k + 1 ) by A6;
F . b1 in the Points of (G_ ((k + 1),X)) ;
then A37: ex B11 being Subset of X st
( F . b1 = B11 & card B11 = k + 1 ) by A6;
F . A in the Lines of (G_ ((k + 1),X)) ;
then A38: ex L1 being Subset of X st
( F . A = L1 & card L1 = (k + 1) + 1 ) by A17;
then A39: F . A is finite ;
F . b1 <> F . b2 by ;
then A40: (k + 1) + 1 c= card ((F . b1) \/ (F . b2)) by ;
b1 on A by A5, A20, A22, A26, Th10;
then F . b1 on F . A by A10;
then A41: F . b1 c= F . A by ;
then (F . b1) \/ (F . b2) c= F . A by ;
then card ((F . b1) \/ (F . b2)) c= k + 2 by ;
then card ((F . b1) \/ (F . b2)) = k + 2 by ;
then A42: (F . b1) \/ (F . b2) = F . A by ;
A43: (incprojmap ((k + 1),f)) . A = f .: x by ;
A44: ( (f .: b1) \/ (f .: b2) = f .: (b1 \/ b2) & F . b2 = (incprojmap ((k + 1),f)) . b2 ) by ;
( F . b1 = (incprojmap ((k + 1),f)) . b1 & (incprojmap ((k + 1),f)) . b1 = f .: b1 ) by ;
hence the line-map of F . x = the line-map of (incprojmap ((k + 1),f)) . x by A5, A20, A35, A42, A43, A44, Def14; :: thesis: verum
end;
A45: ( dom the line-map of F = the Lines of (G_ ((k + 1),X)) & dom the line-map of (incprojmap ((k + 1),f)) = the Lines of (G_ ((k + 1),X)) ) by FUNCT_2:52;
dom the point-map of (incprojmap ((k + 1),f)) = the Points of (G_ ((k + 1),X)) by FUNCT_2:52;
then the point-map of F = the point-map of (incprojmap ((k + 1),f)) by ;
hence IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f) by ; :: thesis: verum