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
ex H being IncProjMap over G_ (k,X), G_ (k,X) st
( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )

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
ex H being IncProjMap over G_ (k,X), G_ (k,X) st
( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) ) )

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
ex H being IncProjMap over G_ (k,X), G_ (k,X) st
( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )

let F be IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X); :: thesis: ( F is automorphism implies ex H being IncProjMap over G_ (k,X), G_ (k,X) st
( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) ) )

assume A3: F is automorphism ; :: thesis: ex H being IncProjMap over G_ (k,X), G_ (k,X) st
( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )

0 + 2 < k + (1 + 1) by ;
then 0 + 2 < (k + 1) + 1 ;
then A4: 2 <= k + 1 by NAT_1:13;
defpred S1[ object , object ] means ex B being finite set st
( B = \$1 & \$2 = meet (F .: (^^ (B,X,(k + 1)))) );
(k + 1) + 0 <= (k + 1) + 2 by XREAL_1:6;
then Segm (k + 1) c= Segm (k + 3) by NAT_1:39;
then A5: k + 1 c= card X by A2;
then A6: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by ;
A7: for e being object st e in the Points of (G_ (k,X)) holds
ex u being object st S1[e,u]
proof
let e be object ; :: thesis: ( e in the Points of (G_ (k,X)) implies ex u being object st S1[e,u] )
assume e in the Points of (G_ (k,X)) ; :: thesis: ex u being object st S1[e,u]
then ex B being Subset of X st
( B = e & card B = k ) by A6;
then reconsider B = e as finite Subset of X ;
take meet (F .: (^^ (B,X,(k + 1)))) ; :: thesis: S1[e, meet (F .: (^^ (B,X,(k + 1))))]
thus S1[e, meet (F .: (^^ (B,X,(k + 1))))] ; :: thesis: verum
end;
consider Hp being Function such that
A8: dom Hp = the Points of (G_ (k,X)) and
A9: for e being object st e in the Points of (G_ (k,X)) holds
S1[e,Hp . e] from A10: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A5, Def1;
(k + 1) + 1 <= (k + 1) + 2 by XREAL_1:6;
then Segm (k + 2) c= Segm (k + 3) by NAT_1:39;
then A11: (k + 1) + 1 c= card X by A2;
then A12: the Points of (G_ ((k + 1),X)) = { A where A is Subset of X : card A = k + 1 } by Def1;
then reconsider Hl = the point-map of F as Function of the Lines of (G_ (k,X)), the Lines of (G_ (k,X)) by A10;
A13: (k + 1) + 2 c= card X by A2;
rng Hp c= the Points of (G_ (k,X))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng Hp or y in the Points of (G_ (k,X)) )
assume y in rng Hp ; :: thesis: y in the Points of (G_ (k,X))
then consider x being object such that
A14: x in dom Hp and
A15: y = Hp . x by FUNCT_1:def 3;
consider B being finite set such that
A16: B = x and
A17: y = meet (F .: (^^ (B,X,(k + 1)))) by A8, A9, A14, A15;
A18: ex x1 being Subset of X st
( x = x1 & card x1 = k ) by A6, A8, A14;
^^ (B,X,(k + 1)) is STAR by ;
then F .: (^^ (B,X,(k + 1))) is STAR by A3, A4, A13, Th23;
then consider S being Subset of X such that
A19: card S = (k + 1) - 1 and
A20: F .: (^^ (B,X,(k + 1))) = { C where C is Subset of X : ( card C = k + 1 & S c= C ) } ;
S = meet (F .: (^^ (B,X,(k + 1)))) by ;
hence y in the Points of (G_ (k,X)) by A6, A17, A19; :: thesis: verum
end;
then reconsider Hp = Hp as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by ;
A21: the point-map of F is bijective by A3;
A22: Hp is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom Hp or not x2 in dom Hp or not Hp . x1 = Hp . x2 or x1 = x2 )
assume that
A23: x1 in dom Hp and
A24: x2 in dom Hp and
A25: Hp . x1 = Hp . x2 ; :: thesis: x1 = x2
consider X2 being finite set such that
A26: X2 = x2 and
A27: Hp . x2 = meet (F .: (^^ (X2,X,(k + 1)))) by ;
A28: ex x12 being Subset of X st
( x2 = x12 & card x12 = k ) by A6, A8, A24;
then A29: card X2 = (k + 1) - 1 by A26;
then A30: meet (^^ (X2,X,(k + 1))) = X2 by ;
^^ (X2,X,(k + 1)) is STAR by ;
then A31: F .: (^^ (X2,X,(k + 1))) is STAR by A3, A4, A13, Th23;
consider X1 being finite set such that
A32: X1 = x1 and
A33: Hp . x1 = meet (F .: (^^ (X1,X,(k + 1)))) by ;
A34: ex x11 being Subset of X st
( x1 = x11 & card x11 = k ) by A6, A8, A23;
^^ (X1,X,(k + 1)) is STAR by ;
then A35: F .: (^^ (X1,X,(k + 1))) is STAR by A3, A4, A13, Th23;
meet (^^ (X1,X,(k + 1))) = X1 by A11, A32, A34, A29, Th30;
hence x1 = x2 by A11, A21, A25, A32, A33, A26, A27, A35, A31, A30, Th6, Th28; :: thesis: verum
end;
take H = IncProjMap(# Hp,Hl #); :: thesis: ( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )

A36: dom the point-map of F = the Points of (G_ ((k + 1),X)) by FUNCT_2:52;
A37: H is incidence_preserving
proof
let A1 be POINT of (G_ (k,X)); :: according to COMBGRAS:def 8 :: thesis: for L1 being LINE of (G_ (k,X)) holds
( A1 on L1 iff H . A1 on H . L1 )

let L1 be LINE of (G_ (k,X)); :: thesis: ( A1 on L1 iff H . A1 on H . L1 )
A38: S1[A1,Hp . A1] by A9;
L1 in the Lines of (G_ (k,X)) ;
then A39: ex l1 being Subset of X st
( l1 = L1 & card l1 = k + 1 ) by A10;
A1 in the Points of (G_ (k,X)) ;
then consider a1 being Subset of X such that
A40: a1 = A1 and
A41: card a1 = k by A6;
consider L11 being POINT of (G_ ((k + 1),X)) such that
A42: L11 = L1 by ;
reconsider a1 = a1 as finite Subset of X by A41;
A43: card a1 = (k + 1) - 1 by A41;
A44: ( H . A1 on H . L1 implies A1 on L1 )
proof
( F " (F .: (^^ (a1,X,(k + 1)))) c= ^^ (a1,X,(k + 1)) & ^^ (a1,X,(k + 1)) c= F " (F .: (^^ (a1,X,(k + 1)))) ) by ;
then A45: F " (F .: (^^ (a1,X,(k + 1)))) = ^^ (a1,X,(k + 1)) by XBOOLE_0:def 10;
H . L1 in the Lines of (G_ (k,X)) ;
then A46: ex hl1 being Subset of X st
( hl1 = H . L1 & card hl1 = k + 1 ) by A10;
^^ (a1,X,(k + 1)) is STAR by ;
then F .: (^^ (a1,X,(k + 1))) is STAR by A3, A4, A13, Th23;
then consider S being Subset of X such that
A47: card S = (k + 1) - 1 and
A48: F .: (^^ (a1,X,(k + 1))) = { A where A is Subset of X : ( card A = k + 1 & S c= A ) } ;
H . A1 in the Points of (G_ (k,X)) ;
then consider ha1 being Subset of X such that
A49: ha1 = H . A1 and
A50: card ha1 = k by A6;
reconsider ha1 = ha1, S = S as finite Subset of X by ;
A51: ^^ (ha1,X,(k + 1)) = ^^ (ha1,X) by ;
assume H . A1 on H . L1 ; :: thesis: A1 on L1
then H . A1 c= H . L1 by A1, A5, Th10;
then F . L11 in ^^ (ha1,X,(k + 1)) by A42, A49, A50, A46, A51;
then L1 in F " (^^ (ha1,X,(k + 1))) by ;
then A52: meet (F " (^^ (ha1,X,(k + 1)))) c= L1 by SETFAM_1:3;
^^ (S,X,(k + 1)) = ^^ (S,X) by ;
then A53: S = meet (F .: (^^ (a1,X,(k + 1)))) by ;
meet (^^ (a1,X,(k + 1))) = a1 by ;
hence A1 on L1 by A1, A5, A40, A38, A49, A50, A48, A51, A53, A52, A45, Th10; :: thesis: verum
end;
A54: ^^ (a1,X,(k + 1)) = ^^ (a1,X) by ;
( A1 on L1 implies H . A1 on H . L1 )
proof
assume A1 on L1 ; :: thesis: H . A1 on H . L1
then A1 c= L1 by A1, A5, Th10;
then L1 in ^^ (a1,X,(k + 1)) by A40, A41, A39, A54;
then F . L11 in F .: (^^ (a1,X,(k + 1))) by ;
then meet (F .: (^^ (a1,X,(k + 1)))) c= F . L11 by SETFAM_1:3;
hence H . A1 on H . L1 by A1, A5, A40, A42, A38, Th10; :: thesis: verum
end;
hence ( A1 on L1 iff H . A1 on H . L1 ) by A44; :: thesis: verum
end;
A55: rng the point-map of F = the Points of (G_ ((k + 1),X)) by ;
for y being object st y in the Points of (G_ (k,X)) holds
ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x )
proof
let y be object ; :: thesis: ( y in the Points of (G_ (k,X)) implies ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x ) )

assume y in the Points of (G_ (k,X)) ; :: thesis: ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x )

then A56: ex Y1 being Subset of X st
( y = Y1 & card Y1 = k ) by A6;
then reconsider y = y as finite Subset of X ;
A57: card y = (k + 1) - 1 by A56;
then ^^ (y,X,(k + 1)) is STAR by ;
then F " (^^ (y,X,(k + 1))) is STAR by A3, A4, A13, Th23;
then consider S being Subset of X such that
A58: card S = (k + 1) - 1 and
A59: F " (^^ (y,X,(k + 1))) = { A where A is Subset of X : ( card A = k + 1 & S c= A ) } ;
A60: S in the Points of (G_ (k,X)) by ;
reconsider S = S as finite Subset of X by A58;
A61: S1[S,Hp . S] by ;
^^ (S,X,(k + 1)) = ^^ (S,X) by ;
then Hp . S = meet (^^ (y,X,(k + 1))) by ;
then y = Hp . S by ;
hence ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x ) by A60; :: thesis: verum
end;
then rng Hp = the Points of (G_ (k,X)) by FUNCT_2:10;
then A62: Hp is onto by FUNCT_2:def 3;
A63: for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
Hp . A = meet (F .: (^^ (B,X,(k + 1))))
proof
let A be POINT of (G_ (k,X)); :: thesis: for B being finite set st B = A holds
Hp . A = meet (F .: (^^ (B,X,(k + 1))))

A64: S1[A,Hp . A] by A9;
let B be finite set ; :: thesis: ( B = A implies Hp . A = meet (F .: (^^ (B,X,(k + 1)))) )
assume A = B ; :: thesis: Hp . A = meet (F .: (^^ (B,X,(k + 1))))
hence Hp . A = meet (F .: (^^ (B,X,(k + 1)))) by A64; :: thesis: verum
end;
the line-map of H is bijective by A3, A10, A12;
hence ( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) ) by A63, A22, A62, A37; :: thesis: verum