let k be Element of NAT ; :: thesis:
let X be non empty set ; :: thesis:
assume A1: ( 0 < k & k + 3 c= card X ) ; :: thesis:
let F be IncProjMap of G_ (k + 1),X, G_ (k + 1),X; :: thesis:
assume A2: F is automorphism ; :: thesis:
( (k + 1) + 2 c= card X & (k + 1) + 0 <= (k + 1) + 2 & 0 + 2 < k + (1 + 1) & card k = k & (k + 1) + 1 <= (k + 1) + 2 ) by A1, CARD_1:def 5, XREAL_1:8;
then ( k + 1 c= k + 3 & k + 2 c= k + 3 & 0 + 2 < (k + 1) + 1 & k + 0 < k + 1 ) by NAT_1:40, XREAL_1:10;
then A4: ( k + 1 c= card X & 2 <= k + 1 & (k + 1) + 2 c= card X & (k + 1) + 1 c= card X & 0 < k + 1 ) by A1, NAT_1:13, XBOOLE_1:1;
then A5: the Points of (G_ k,X) = { A where A is Subset of X : card A = k } by A1, Def1;
A6: the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 } by A1, A4, Def1;
A7: the Points of (G_ (k + 1),X) = { A where A is Subset of X : card A = k + 1 } by A4, Def1;
defpred S₁[ set , set ] means ex B being finite set st
( B = $1 & $2 = meet (F .: (^^ B,X,(k + 1))) );
A8: for e being set st e in the Points of (G_ k,X) holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis:
assume e in the Points of (G_ k,X) ; :: thesis:
then consider B being Subset of X such that
A9: ( B = e & card B = k ) by A5;
reconsider B = e as finite Subset of X by A9;
take u = meet (F .: (^^ B,X,(k + 1))); :: thesis:
thus S₁[e,u] ; :: thesis:

end;

consider Hp being Function such that
A10: dom Hp = the Points of (G_ k,X) and
A11: for e being set st e in the Points of (G_ k,X) holds
S₁[e,Hp . e] from CLASSES1:sch 1(A8);
rng Hp c= the Points of (G_ k,X)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A12: y in rng Hp ; :: thesis:
consider x being set such that
A13: ( x in dom Hp & y = Hp . x ) by A12, FUNCT_1:def 5;
consider B being finite set such that
A14: ( B = x & y = meet (F .: (^^ B,X,(k + 1))) ) by A10, A11, A13;
consider x1 being Subset of X such that
A15: ( x = x1 & card x1 = k ) by A5, A10, A13;
( card B = (k + 1) - 1 & B c= X ) by A14, A15;
then ^^ B,X,(k + 1) is STAR by A4, Th29;
then F .: (^^ B,X,(k + 1)) is STAR by A2, A4, Th23;
then consider S being Subset of X such that
A16: ( card S = (k + 1) - 1 & F .: (^^ B,X,(k + 1)) = { C where C is Subset of X : ( card C = k + 1 & S c= C ) } ) by Def4;
( S = meet (F .: (^^ B,X,(k + 1))) & S in the Points of (G_ k,X) ) by A4, A5, A16, Th26;
hence y in the Points of (G_ k,X) by A14; :: thesis:

end;

then reconsider Hp = Hp as Function of the Points of (G_ k,X),the Points of (G_ k,X) by A10, FUNCT_2:4;
the point-map of F is bijective by A2, Def9;
then A17: ( the point-map of F is onto & the point-map of F is one-to-one ) ;
then A18: ( dom the point-map of F = the Points of (G_ (k + 1),X) & rng the point-map of F = the Points of (G_ (k + 1),X) ) by FUNCT_2:67, FUNCT_2:def 3;
reconsider Hl = the point-map of F as Function of the Lines of (G_ k,X),the Lines of (G_ k,X) by A6, A7;
take H = IncProjMap(# Hp,Hl #); :: thesis:
A19: 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:
let B be finite set ; :: thesis:
assume A20: A = B ; :: thesis:
S₁[A,Hp . A] by A11;
hence Hp . A = meet (F .: (^^ B,X,(k + 1))) by A20; :: thesis:

end;

H is automorphism

proof

A21: the line-map of H is bijective by A2, A6, A7, Def9;
A22: the point-map of H is bijective

proof

A23: Hp is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume A24: ( x1 in dom Hp & x2 in dom Hp & Hp . x1 = Hp . x2 ) ; :: thesis:
consider X1 being finite set such that
A25: ( X1 = x1 & Hp . x1 = meet (F .: (^^ X1,X,(k + 1))) ) by A11, A24;
consider X2 being finite set such that
A26: ( X2 = x2 & Hp . x2 = meet (F .: (^^ X2,X,(k + 1))) ) by A11, A24;
consider x11 being Subset of X such that
A27: ( x1 = x11 & card x11 = k ) by A5, A10, A24;
( card X1 = (k + 1) - 1 & X1 c= X ) by A25, A27;
then ^^ X1,X,(k + 1) is STAR by A4, Th29;
then A28: F .: (^^ X1,X,(k + 1)) is STAR by A2, A4, Th23;
consider x12 being Subset of X such that
A29: ( x2 = x12 & card x12 = k ) by A5, A10, A24;
A30: ( card X2 = (k + 1) - 1 & X2 c= X ) by A26, A29;
then ^^ X2,X,(k + 1) is STAR by A4, Th29;
then A31: F .: (^^ X2,X,(k + 1)) is STAR by A2, A4, Th23;
( meet (^^ X1,X,(k + 1)) = X1 & meet (^^ X2,X,(k + 1)) = X2 ) by A4, A25, A27, A30, Th30;
hence x1 = x2 by A4, A17, A24, A25, A26, A28, A31, Th6, Th28; :: thesis:

end;

for y being set st y in the Points of (G_ k,X) holds
ex x being set st
( x in the Points of (G_ k,X) & y = Hp . x )

proof

let y be set ; :: thesis:
assume A32: y in the Points of (G_ k,X) ; :: thesis:
consider Y1 being Subset of X such that
A33: ( y = Y1 & card Y1 = k ) by A5, A32;
reconsider y = y as finite Subset of X by A33;
A34: card y = (k + 1) - 1 by A33;
then ^^ y,X,(k + 1) is STAR by A4, Th29;
then F " (^^ y,X,(k + 1)) is STAR by A2, A4, Th23;
then consider S being Subset of X such that
A35: ( card S = (k + 1) - 1 & F " (^^ y,X,(k + 1)) = { A where A is Subset of X : ( card A = k + 1 & S c= A ) } ) by Def4;
A36: ( S = meet (F " (^^ y,X,(k + 1))) & S in the Points of (G_ k,X) ) by A4, A5, A35, Th26;
reconsider S = S as finite Subset of X by A35;
^^ S,X,(k + 1) = ^^ S,X by A4, A35, Def13;
then ( F " (^^ y,X,(k + 1)) = ^^ S,X,(k + 1) & S₁[S,Hp . S] ) by A11, A35, A36;
then Hp . S = meet (^^ y,X,(k + 1)) by A18, FUNCT_1:147;
then y = Hp . S by A4, A34, Th30;
hence ex x being set st
( x in the Points of (G_ k,X) & y = Hp . x ) by A36; :: thesis:

end;

then rng Hp = the Points of (G_ k,X) by FUNCT_2:16;
then Hp is onto by FUNCT_2:def 3;
hence the point-map of H is bijective by A23; :: thesis:

end;

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:
A1 in the Points of (G_ k,X) ;
then consider a1 being Subset of X such that
A37: ( a1 = A1 & card a1 = k ) by A5;
L1 in the Lines of (G_ k,X) ;
then consider l1 being Subset of X such that
A38: ( l1 = L1 & card l1 = k + 1 ) by A6;
L1 in the Points of (G_ (k + 1),X) by A7, A38;
then consider L11 being POINT of (G_ (k + 1),X) such that
A39: L11 = L1 ;
reconsider a1 = a1 as finite Subset of X by A37;
A40: S₁[A1,Hp . A1] by A11;
A41: card a1 = (k + 1) - 1 by A37;
then A42: ^^ a1,X,(k + 1) = ^^ a1,X by A4, Def13;
A43: ( A1 on L1 implies H . A1 on H . L1 )

proof

assume A1 on L1 ; :: thesis:
then A1 c= L1 by A1, A4, Th10;
then L1 in ^^ a1,X,(k + 1) by A37, A38, A42;
then F . L11 in F .: (^^ a1,X,(k + 1)) by A18, A39, FUNCT_1:def 12;
then ( meet (F .: (^^ a1,X,(k + 1))) c= F . L11 & H . L1 = F . L11 ) by A39, SETFAM_1:4;
hence H . A1 on H . L1 by A1, A4, A37, A40, Th10; :: thesis:

end;

( H . A1 on H . L1 implies A1 on L1 )

proof

assume H . A1 on H . L1 ; :: thesis:
then A44: H . A1 c= H . L1 by A1, A4, Th10;
H . A1 in the Points of (G_ k,X) ;
then consider ha1 being Subset of X such that
A45: ( ha1 = H . A1 & card ha1 = k ) by A5;
H . L1 in the Lines of (G_ k,X) ;
then consider hl1 being Subset of X such that
A46: ( hl1 = H . L1 & card hl1 = k + 1 ) by A6;
^^ a1,X,(k + 1) is STAR by A4, A41, Th29;
then F .: (^^ a1,X,(k + 1)) is STAR by A2, A4, Th23;
then consider S being Subset of X such that
A47: ( card S = (k + 1) - 1 & F .: (^^ a1,X,(k + 1)) = { A where A is Subset of X : ( card A = k + 1 & S c= A ) } ) by Def4;
reconsider ha1 = ha1, S = S as finite Subset of X by A45, A47;
A48: ( ^^ ha1,X,(k + 1) = ^^ ha1,X & ^^ S,X,(k + 1) = ^^ S,X ) by A4, A45, A47, Def13;
then ( F . L11 in ^^ ha1,X,(k + 1) & F .: (^^ a1,X,(k + 1)) = ^^ S,X,(k + 1) ) by A39, A44, A45, A46, A47;
then ( L1 in F " (^^ ha1,X,(k + 1)) & F " (F .: (^^ a1,X,(k + 1))) c= ^^ a1,X,(k + 1) & ^^ a1,X,(k + 1) c= F " (F .: (^^ a1,X,(k + 1))) & S = meet (F .: (^^ a1,X,(k + 1))) ) by A4, A17, A18, A39, A47, Th30, FUNCT_1:146, FUNCT_1:152, FUNCT_1:def 13;
then ( meet (F " (^^ ha1,X,(k + 1))) c= L1 & F " (F .: (^^ a1,X,(k + 1))) = ^^ a1,X,(k + 1) & meet (^^ a1,X,(k + 1)) = a1 & ^^ ha1,X,(k + 1) = F .: (^^ a1,X,(k + 1)) ) by A4, A37, A40, A45, A47, A48, Th30, SETFAM_1:4, XBOOLE_0:def 10;
hence A1 on L1 by A1, A4, A37, Th10; :: thesis:

end;

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

end;

hence H is automorphism by A21, A22, Def9; :: thesis:

end;

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 A19; :: thesis: