let k be Nat; :: thesis:
let X be non empty set ; :: thesis:
assume that
A1: 0 < k and
A2: k + 3 c= card X ; :: thesis:
let F be IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X); :: thesis:
assume A3: F is automorphism ; :: thesis:
0 + 2 < k + (1 + 1) by A1, XREAL_1:6;
then 0 + 2 < (k + 1) + 1 ;
then A4: 2 <= k + 1 by NAT_1:13;
defpred S₁[ 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 A1, Def1;
A7: for e being object st e in the Points of (G_ (k,X)) holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis:
assume e in the Points of (G_ (k,X)) ; :: thesis:
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:
thus S₁[e, meet (F .: (^^ (B,X,(k + 1))))] ; :: thesis:

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
S₁[e,Hp . e] from CLASSES1:sch 1(A7);
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:
assume y in rng Hp ; :: thesis:
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 A11, A16, A18, Th29;
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 A11, A19, A20, Th26;
hence y in the Points of (G_ (k,X)) by A6, A17, A19; :: thesis:

end;

then reconsider Hp = Hp as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by A8, FUNCT_2:2;
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:
assume that
A23: x1 in dom Hp and
A24: x2 in dom Hp and
A25: Hp . x1 = Hp . x2 ; :: thesis:
consider X2 being finite set such that
A26: X2 = x2 and
A27: Hp . x2 = meet (F .: (^^ (X2,X,(k + 1)))) by A9, A24;
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 A11, A26, A28, Th30;
^^ (X2,X,(k + 1)) is STAR by A11, A26, A28, Th29;
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 A9, A23;
A34: ex x11 being Subset of X st
( x1 = x11 & card x11 = k ) by A6, A8, A23;
^^ (X1,X,(k + 1)) is STAR by A11, A32, A34, Th29;
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:

end;

take H = IncProjMap(# Hp,Hl #); :: thesis:
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:
let L1 be LINE of (G_ (k,X)); :: thesis:
A38: S₁[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 A10, A12;
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 A21, A36, FUNCT_1:76, FUNCT_1:82;
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 A11, A43, Th29;
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 A50, A47;
A51: ^^ (ha1,X,(k + 1)) = ^^ (ha1,X) by A11, A50, A47, Def13;
assume H . A1 on H . L1 ; :: thesis:
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 A36, A42, FUNCT_1:def 7;
then A52: meet (F " (^^ (ha1,X,(k + 1)))) c= L1 by SETFAM_1:3;
^^ (S,X,(k + 1)) = ^^ (S,X) by A11, A47, Def13;
then A53: S = meet (F .: (^^ (a1,X,(k + 1)))) by A11, A47, A48, Th30;
meet (^^ (a1,X,(k + 1))) = a1 by A11, A41, A47, Th30;
hence A1 on L1 by A1, A5, A40, A38, A49, A50, A48, A51, A53, A52, A45, Th10; :: thesis:

end;

A54: ^^ (a1,X,(k + 1)) = ^^ (a1,X) by A11, A43, Def13;
( A1 on L1 implies H . A1 on H . L1 )

proof

assume A1 on L1 ; :: thesis:
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 A36, A42, FUNCT_1:def 6;
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:

end;

hence ( A1 on L1 iff H . A1 on H . L1 ) by A44; :: thesis:

end;

A55: rng the point-map of F = the Points of (G_ ((k + 1),X)) by A21, FUNCT_2:def 3;
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:
assume y in the Points of (G_ (k,X)) ; :: thesis:
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 A11, Th29;
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 A6, A58;
reconsider S = S as finite Subset of X by A58;
A61: S₁[S,Hp . S] by A9, A60;
^^ (S,X,(k + 1)) = ^^ (S,X) by A11, A58, Def13;
then Hp . S = meet (^^ (y,X,(k + 1))) by A55, A58, A59, A61, FUNCT_1:77;
then y = Hp . S by A11, A57, Th30;
hence ex x being object st
( x in the Points of (G_ (k,X)) & y = Hp . x ) by A60; :: thesis:

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:
A64: S₁[A,Hp . A] by A9;
let B be finite set ; :: thesis:
assume A = B ; :: thesis:
hence Hp . A = meet (F .: (^^ (B,X,(k + 1)))) by A64; :: thesis:

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: