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 A1, XREAL_1:6;

then 0 + 2 < (k + 1) + 1 ;

then A4: 2 <= k + 1 by NAT_1:13;

defpred S_{1}[ 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_{1}[e,u]

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_{1}[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))

A21: the point-map of F is bijective by A3;

A22: Hp is one-to-one

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

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 )

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))))

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

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 A1, XREAL_1:6;

then 0 + 2 < (k + 1) + 1 ;

then A4: 2 <= k + 1 by NAT_1:13;

defpred S

( 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

proof

consider Hp being Function such that
let e be object ; :: thesis: ( e in the Points of (G_ (k,X)) implies ex u being object st S_{1}[e,u] )

assume e in the Points of (G_ (k,X)) ; :: thesis: ex u being object st S_{1}[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: S_{1}[e, meet (F .: (^^ (B,X,(k + 1))))]

thus S_{1}[e, meet (F .: (^^ (B,X,(k + 1))))]
; :: thesis: verum

end;assume e in the Points of (G_ (k,X)) ; :: thesis: ex u being object st S

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: S

thus S

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

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

then reconsider Hp = Hp as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by A8, FUNCT_2:2;
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 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: verum

end;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 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: verum

A21: the point-map of F is bijective by A3;

A22: Hp is one-to-one

proof

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))
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 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: verum

end;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 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: verum

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

A55:
rng the point-map of F = the Points of (G_ ((k + 1),X))
by A21, FUNCT_2:def 3;
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: S_{1}[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 )

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

end;( 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: S

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

A54:
^^ (a1,X,(k + 1)) = ^^ (a1,X)
by A11, A43, Def13;
( 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: 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 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: verum

end;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: 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 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: verum

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

proof

hence
( A1 on L1 iff H . A1 on H . L1 )
by A44; :: thesis: verum
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 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: verum

end;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: verum

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

then
rng Hp = the Points of (G_ (k,X))
by FUNCT_2:10;
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 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_{1}[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: verum

end;( 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 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,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: verum

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

the line-map of H is bijective
by A3, A10, A12;
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: S_{1}[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;Hp . A = meet (F .: (^^ (B,X,(k + 1))))

A64: S

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

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