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 A1, Def1;

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

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

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 A12, A14;

hence IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f) by A45, A19, FUNCT_1:def 11; :: thesis: verum

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 A1, Def1;

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

A17:
the Lines of (G_ ((k + 1),X)) = { L where L is Subset of X : card L = (k + 1) + 1 }
by A5, Def1;
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 A1, A3, Def14;

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;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 A1, A3, Def14;

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

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

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;
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 A8, CARD_FIL:36;

A24: x is finite by A21;

then A25: card (x \ B1) = (k + 2) - (k + 1) by A21, A22, A23, CARD_2:44;

B1 c= X by A21, A22, XBOOLE_1:1;

then B1 in the Points of (G_ ((k + 1),X)) by A6, A23;

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 A7, A23, CARD_FIL:36;

B1 is finite by A23;

then A29: card (C1 \/ (x \ B1)) = k + 1 by A27, A28, A24, A25, CARD_2:40, XBOOLE_1:85;

C1 c= x by A22, A27;

then A30: C1 \/ (x \ B1) c= x by XBOOLE_1:8;

then C1 \/ (x \ B1) c= X by A21, XBOOLE_1:1;

then C1 \/ (x \ B1) in the Points of (G_ ((k + 1),X)) by A6, A29;

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 A5, Th10;

B1 \/ (C1 \/ (x \ B1)) c= x by A22, A30, XBOOLE_1:8;

then A33: card (b1 \/ b2) c= k + 2 by A21, A26, A31, CARD_1:11;

B1 misses x \ B1 by XBOOLE_1:79;

then card ((x \ B1) /\ B1) = 0 by CARD_1:27, XBOOLE_0:def 7;

then A34: b1 <> b2 by A25, A26, A31, XBOOLE_1:11, XBOOLE_1:28;

then (k + 1) + 1 c= card (b1 \/ b2) by A23, A29, A26, A31, Th1;

then card (b1 \/ b2) = k + 2 by A33, XBOOLE_0:def 10;

then A35: b1 \/ b2 = x by A21, A22, A24, A30, A26, A31, CARD_2:102, XBOOLE_1:8;

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 A18, A12, A34, FUNCT_1:def 4;

then A40: (k + 1) + 1 c= card ((F . b1) \/ (F . b2)) by A37, A36, Th1;

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 A5, Th10;

then (F . b1) \/ (F . b2) c= F . A by A32, XBOOLE_1:8;

then card ((F . b1) \/ (F . b2)) c= k + 2 by A38, CARD_1:11;

then card ((F . b1) \/ (F . b2)) = k + 2 by A40, XBOOLE_0:def 10;

then A42: (F . b1) \/ (F . b2) = F . A by A41, A32, A38, A39, CARD_2:102, XBOOLE_1:8;

A43: (incprojmap ((k + 1),f)) . A = f .: x by A5, A20, Def14;

A44: ( (f .: b1) \/ (f .: b2) = f .: (b1 \/ b2) & F . b2 = (incprojmap ((k + 1),f)) . b2 ) by A12, A14, RELAT_1:120;

( F . b1 = (incprojmap ((k + 1),f)) . b1 & (incprojmap ((k + 1),f)) . b1 = f .: b1 ) by A5, A12, A14, Def14;

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;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 A8, CARD_FIL:36;

A24: x is finite by A21;

then A25: card (x \ B1) = (k + 2) - (k + 1) by A21, A22, A23, CARD_2:44;

B1 c= X by A21, A22, XBOOLE_1:1;

then B1 in the Points of (G_ ((k + 1),X)) by A6, A23;

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 A7, A23, CARD_FIL:36;

B1 is finite by A23;

then A29: card (C1 \/ (x \ B1)) = k + 1 by A27, A28, A24, A25, CARD_2:40, XBOOLE_1:85;

C1 c= x by A22, A27;

then A30: C1 \/ (x \ B1) c= x by XBOOLE_1:8;

then C1 \/ (x \ B1) c= X by A21, XBOOLE_1:1;

then C1 \/ (x \ B1) in the Points of (G_ ((k + 1),X)) by A6, A29;

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 A5, Th10;

B1 \/ (C1 \/ (x \ B1)) c= x by A22, A30, XBOOLE_1:8;

then A33: card (b1 \/ b2) c= k + 2 by A21, A26, A31, CARD_1:11;

B1 misses x \ B1 by XBOOLE_1:79;

then card ((x \ B1) /\ B1) = 0 by CARD_1:27, XBOOLE_0:def 7;

then A34: b1 <> b2 by A25, A26, A31, XBOOLE_1:11, XBOOLE_1:28;

then (k + 1) + 1 c= card (b1 \/ b2) by A23, A29, A26, A31, Th1;

then card (b1 \/ b2) = k + 2 by A33, XBOOLE_0:def 10;

then A35: b1 \/ b2 = x by A21, A22, A24, A30, A26, A31, CARD_2:102, XBOOLE_1:8;

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 A18, A12, A34, FUNCT_1:def 4;

then A40: (k + 1) + 1 c= card ((F . b1) \/ (F . b2)) by A37, A36, Th1;

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 A5, Th10;

then (F . b1) \/ (F . b2) c= F . A by A32, XBOOLE_1:8;

then card ((F . b1) \/ (F . b2)) c= k + 2 by A38, CARD_1:11;

then card ((F . b1) \/ (F . b2)) = k + 2 by A40, XBOOLE_0:def 10;

then A42: (F . b1) \/ (F . b2) = F . A by A41, A32, A38, A39, CARD_2:102, XBOOLE_1:8;

A43: (incprojmap ((k + 1),f)) . A = f .: x by A5, A20, Def14;

A44: ( (f .: b1) \/ (f .: b2) = f .: (b1 \/ b2) & F . b2 = (incprojmap ((k + 1),f)) . b2 ) by A12, A14, RELAT_1:120;

( F . b1 = (incprojmap ((k + 1),f)) . b1 & (incprojmap ((k + 1),f)) . b1 = f .: b1 ) by A5, A12, A14, Def14;

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

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 A12, A14;

hence IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f) by A45, A19, FUNCT_1:def 11; :: thesis: verum