let k be Element of NAT ; :: thesis: for X being non empty set st 2 <= k & k + 2 c= card X holds

for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR )

let X be non empty set ; :: thesis: ( 2 <= k & k + 2 c= card X implies for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR ) )

assume that

A1: 2 <= k and

A2: k + 2 c= card X ; :: thesis: for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR )

let F be IncProjMap over G_ (k,X), G_ (k,X); :: thesis: ( F is automorphism implies for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR ) )

assume A3: F is automorphism ; :: thesis: for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR )

A4: k - 1 is Element of NAT by A1, NAT_1:21, XXREAL_0:2;

then reconsider k1 = k - 1 as Nat ;

A5: succ (Segm k1) = Segm (k1 + 1) by NAT_1:38;

2 - 1 <= k - 1 by A1, XREAL_1:9;

then A6: Segm 1 c= Segm k1 by NAT_1:39;

A7: 1 <= k by A1, XXREAL_0:2;

then A8: Segm 1 c= Segm k by NAT_1:39;

let K be Subset of the Points of (G_ (k,X)); :: thesis: ( K is STAR implies ( F .: K is STAR & F " K is STAR ) )

assume A9: K is STAR ; :: thesis: ( F .: K is STAR & F " K is STAR )

then A10: K is maximal_clique by A1, A2, Th14;

then A11: K is clique ;

k + 1 <= k + 2 by XREAL_1:7;

then Segm (k + 1) c= Segm (k + 2) by NAT_1:39;

then A12: k + 1 c= card X by A2;

then A13: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, Def1;

A14: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A12, Def1;

A15: k + 0 <= k + 1 by XREAL_1:7;

then 1 <= k + 1 by A7, XXREAL_0:2;

then A16: Segm 1 c= Segm (k + 1) by NAT_1:39;

A17: not F " K is TOP

hence ( F .: K is STAR & F " K is STAR ) by A1, A2, A84, A17, Th15; :: thesis: verum

for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR )

let X be non empty set ; :: thesis: ( 2 <= k & k + 2 c= card X implies for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR ) )

assume that

A1: 2 <= k and

A2: k + 2 c= card X ; :: thesis: for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR )

let F be IncProjMap over G_ (k,X), G_ (k,X); :: thesis: ( F is automorphism implies for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR ) )

assume A3: F is automorphism ; :: thesis: for K being Subset of the Points of (G_ (k,X)) st K is STAR holds

( F .: K is STAR & F " K is STAR )

A4: k - 1 is Element of NAT by A1, NAT_1:21, XXREAL_0:2;

then reconsider k1 = k - 1 as Nat ;

A5: succ (Segm k1) = Segm (k1 + 1) by NAT_1:38;

2 - 1 <= k - 1 by A1, XREAL_1:9;

then A6: Segm 1 c= Segm k1 by NAT_1:39;

A7: 1 <= k by A1, XXREAL_0:2;

then A8: Segm 1 c= Segm k by NAT_1:39;

let K be Subset of the Points of (G_ (k,X)); :: thesis: ( K is STAR implies ( F .: K is STAR & F " K is STAR ) )

assume A9: K is STAR ; :: thesis: ( F .: K is STAR & F " K is STAR )

then A10: K is maximal_clique by A1, A2, Th14;

then A11: K is clique ;

k + 1 <= k + 2 by XREAL_1:7;

then Segm (k + 1) c= Segm (k + 2) by NAT_1:39;

then A12: k + 1 c= card X by A2;

then A13: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, Def1;

A14: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A12, Def1;

A15: k + 0 <= k + 1 by XREAL_1:7;

then 1 <= k + 1 by A7, XXREAL_0:2;

then A16: Segm 1 c= Segm (k + 1) by NAT_1:39;

A17: not F " K is TOP

proof

A84:
not F .: K is TOP
assume
F " K is TOP
; :: thesis: contradiction

then consider B being Subset of X such that

A18: ( card B = k + 1 & F " K = { A where A is Subset of X : ( card A = k & A c= B ) } ) ;

consider X1 being set such that

A19: ( X1 c= B & card X1 = 1 ) by A16, A18, CARD_FIL:36;

A20: B is finite by A18;

then A21: card (B \ X1) = (k + 1) - 1 by A18, A19, CARD_2:44;

then consider X2 being set such that

A22: X2 c= B \ X1 and

A23: card X2 = 1 by A8, CARD_FIL:36;

consider m being Nat such that

A24: m = k - 1 by A4;

A25: card (B \ X2) = (k + 1) - 1 by A18, A20, A22, A23, CARD_2:44, XBOOLE_1:106;

then B \ X2 in the Points of (G_ (k,X)) by A13;

then consider B2 being POINT of (G_ (k,X)) such that

A26: B \ X2 = B2 ;

card ((B \ X1) \ X2) = k - 1 by A20, A21, A22, A23, CARD_2:44;

then consider X3 being set such that

A27: X3 c= (B \ X1) \ X2 and

A28: card X3 = 1 by A6, CARD_FIL:36;

A29: X3 c= B \ (X2 \/ X1) by A27, XBOOLE_1:41;

then A30: card (B \ X3) = (k + 1) - 1 by A18, A20, A28, CARD_2:44, XBOOLE_1:106;

then B \ X3 in the Points of (G_ (k,X)) by A13;

then consider B3 being POINT of (G_ (k,X)) such that

A31: B \ X3 = B3 ;

B in the Lines of (G_ (k,X)) by A14, A18;

then consider L2 being LINE of (G_ (k,X)) such that

A32: B = L2 ;

B \ X1 in the Points of (G_ (k,X)) by A13, A21;

then consider B1 being POINT of (G_ (k,X)) such that

A33: B \ X1 = B1 ;

consider S being Subset of X such that

A34: card S = k - 1 and

A35: K = { A where A is Subset of X : ( card A = k & S c= A ) } by A9;

consider A1 being POINT of (G_ (k,X)) such that

A36: A1 = F . B1 ;

A37: X3 c= (B \ X2) \ X1 by A29, XBOOLE_1:41;

A38: ( B \ X1 <> B \ X2 & B \ X2 <> B \ X3 & B \ X1 <> B \ X3 )

A39: A3 = F . B3 ;

A40: B \ X3 c= B by XBOOLE_1:106;

then B3 in F " K by A18, A30, A31;

then A41: A3 in K by A39, FUNCT_1:def 7;

then A42: ex A13 being Subset of X st

( A3 = A13 & card A13 = k & S c= A13 ) by A35;

A43: B \ X1 c= B by XBOOLE_1:106;

then B1 in F " K by A18, A21, A33;

then A44: A1 in K by A36, FUNCT_1:def 7;

then A45: ex A11 being Subset of X st

( A1 = A11 & card A11 = k & S c= A11 ) by A35;

then A46: card A1 = (k - 1) + 1 ;

consider A2 being POINT of (G_ (k,X)) such that

A47: A2 = F . B2 ;

A48: B \ X2 c= B by XBOOLE_1:106;

then B2 in F " K by A18, A25, A26;

then A49: A2 in K by A47, FUNCT_1:def 7;

then consider L3a being LINE of (G_ (k,X)) such that

A50: {A1,A2} on L3a by A11, A44;

A51: card A1 = (k + 1) - 1 by A45;

A52: F is incidence_preserving by A3;

A53: card ((A1 /\ A2) /\ A3) c= card (A1 /\ A2) by CARD_1:11, XBOOLE_1:17;

consider L1 being LINE of (G_ (k,X)) such that

A54: L1 = F . L2 ;

B1 on L2 by A1, A12, A43, A33, A32, Th10;

then A55: A1 on L1 by A52, A36, A54;

then A56: A1 c= L1 by A1, A12, Th10;

L1 in the Lines of (G_ (k,X)) ;

then A57: ex l12 being Subset of X st

( L1 = l12 & card l12 = k + 1 ) by A14;

B3 on L2 by A1, A12, A40, A31, A32, Th10;

then A58: A3 on L1 by A52, A39, A54;

then A59: A3 c= L1 by A1, A12, Th10;

then A1 \/ A3 c= L1 by A56, XBOOLE_1:8;

then A60: card (A1 \/ A3) c= k + 1 by A57, CARD_1:11;

A61: ex A12 being Subset of X st

( A2 = A12 & card A12 = k & S c= A12 ) by A49, A35;

then A62: card A2 = (k - 1) + 1 ;

B2 on L2 by A1, A12, A48, A26, A32, Th10;

then A63: A2 on L1 by A52, A47, A54;

then A64: A2 c= L1 by A1, A12, Th10;

then A1 \/ A2 c= L1 by A56, XBOOLE_1:8;

then A65: card (A1 \/ A2) c= k + 1 by A57, CARD_1:11;

A66: ( the point-map of F is bijective & the Points of (G_ (k,X)) = dom the point-map of F ) by A3, FUNCT_2:52;

then A67: A1 <> A2 by A38, A33, A26, A36, A47, FUNCT_1:def 4;

then k + 1 c= card (A1 \/ A2) by A45, A61, Th1;

then card (A1 \/ A2) = (k - 1) + (2 * 1) by A65, XBOOLE_0:def 10;

then A68: card (A1 /\ A2) = (k + 1) - 2 by A4, A61, A46, Th2;

{A1,A2} on L1 by A55, A63, INCSP_1:1;

then A69: L1 = L3a by A67, A50, INCSP_1:def 10;

consider L3b being LINE of (G_ (k,X)) such that

A70: {A2,A3} on L3b by A11, A49, A41;

A1 <> A3 by A66, A38, A33, A31, A36, A39, FUNCT_1:def 4;

then k + 1 c= card (A1 \/ A3) by A45, A42, Th1;

then card (A1 \/ A3) = (k - 1) + (2 * 1) by A60, XBOOLE_0:def 10;

then A71: card (A1 /\ A3) = (k + 1) - 2 by A4, A42, A46, Th2;

A3 on L3b by A70, INCSP_1:1;

then A72: A3 c= L3b by A1, A12, Th10;

A2 on L3b by A70, INCSP_1:1;

then A73: A2 c= L3b by A1, A12, Th10;

L3b in the Lines of (G_ (k,X)) ;

then A74: ex l13b being Subset of X st

( L3b = l13b & card l13b = k + 1 ) by A14;

card (A1 /\ A2) in succ (k - 1) by A5, A67, A45, A61, Th1;

then card (A1 /\ A2) c= m by A24, ORDINAL1:22;

then A75: card ((A1 /\ A2) /\ A3) c= m by A53;

S c= A1 /\ A2 by A45, A61, XBOOLE_1:19;

then S c= (A1 /\ A2) /\ A3 by A42, XBOOLE_1:19;

then m c= card ((A1 /\ A2) /\ A3) by A34, A24, CARD_1:11;

then A76: k - 1 = card ((A1 /\ A2) /\ A3) by A24, A75, XBOOLE_0:def 10;

A1 on L3a by A50, INCSP_1:1;

then A77: A1 c= L3a by A1, A12, Th10;

A78: k - 1 <> (k + 1) - 3 ;

A2 \/ A3 c= L1 by A64, A59, XBOOLE_1:8;

then A79: card (A2 \/ A3) c= k + 1 by A57, CARD_1:11;

A80: A2 <> A3 by A66, A38, A26, A31, A47, A39, FUNCT_1:def 4;

then k + 1 c= card (A2 \/ A3) by A61, A42, Th1;

then card (A2 \/ A3) = (k - 1) + (2 * 1) by A79, XBOOLE_0:def 10;

then A81: card (A2 /\ A3) = (k + 1) - 2 by A4, A42, A62, Th2;

( 2 + 1 <= k + 1 & 2 <= k + 1 ) by A1, A15, XREAL_1:6, XXREAL_0:2;

then A82: card ((A1 \/ A2) \/ A3) = (k + 1) + 1 by A61, A42, A76, A68, A51, A81, A71, A78, Th7;

A83: L3a <> L3b

hence contradiction by A80, A70, A83, A69, INCSP_1:def 10; :: thesis: verum

end;then consider B being Subset of X such that

A18: ( card B = k + 1 & F " K = { A where A is Subset of X : ( card A = k & A c= B ) } ) ;

consider X1 being set such that

A19: ( X1 c= B & card X1 = 1 ) by A16, A18, CARD_FIL:36;

A20: B is finite by A18;

then A21: card (B \ X1) = (k + 1) - 1 by A18, A19, CARD_2:44;

then consider X2 being set such that

A22: X2 c= B \ X1 and

A23: card X2 = 1 by A8, CARD_FIL:36;

consider m being Nat such that

A24: m = k - 1 by A4;

A25: card (B \ X2) = (k + 1) - 1 by A18, A20, A22, A23, CARD_2:44, XBOOLE_1:106;

then B \ X2 in the Points of (G_ (k,X)) by A13;

then consider B2 being POINT of (G_ (k,X)) such that

A26: B \ X2 = B2 ;

card ((B \ X1) \ X2) = k - 1 by A20, A21, A22, A23, CARD_2:44;

then consider X3 being set such that

A27: X3 c= (B \ X1) \ X2 and

A28: card X3 = 1 by A6, CARD_FIL:36;

A29: X3 c= B \ (X2 \/ X1) by A27, XBOOLE_1:41;

then A30: card (B \ X3) = (k + 1) - 1 by A18, A20, A28, CARD_2:44, XBOOLE_1:106;

then B \ X3 in the Points of (G_ (k,X)) by A13;

then consider B3 being POINT of (G_ (k,X)) such that

A31: B \ X3 = B3 ;

B in the Lines of (G_ (k,X)) by A14, A18;

then consider L2 being LINE of (G_ (k,X)) such that

A32: B = L2 ;

B \ X1 in the Points of (G_ (k,X)) by A13, A21;

then consider B1 being POINT of (G_ (k,X)) such that

A33: B \ X1 = B1 ;

consider S being Subset of X such that

A34: card S = k - 1 and

A35: K = { A where A is Subset of X : ( card A = k & S c= A ) } by A9;

consider A1 being POINT of (G_ (k,X)) such that

A36: A1 = F . B1 ;

A37: X3 c= (B \ X2) \ X1 by A29, XBOOLE_1:41;

A38: ( B \ X1 <> B \ X2 & B \ X2 <> B \ X3 & B \ X1 <> B \ X3 )

proof

consider A3 being POINT of (G_ (k,X)) such that
assume
( B \ X1 = B \ X2 or B \ X2 = B \ X3 or B \ X1 = B \ X3 )
; :: thesis: contradiction

then ( X2 = {} or X3 = {} or X3 = {} ) by A22, A27, A37, XBOOLE_1:38, XBOOLE_1:106;

hence contradiction by A23, A28; :: thesis: verum

end;then ( X2 = {} or X3 = {} or X3 = {} ) by A22, A27, A37, XBOOLE_1:38, XBOOLE_1:106;

hence contradiction by A23, A28; :: thesis: verum

A39: A3 = F . B3 ;

A40: B \ X3 c= B by XBOOLE_1:106;

then B3 in F " K by A18, A30, A31;

then A41: A3 in K by A39, FUNCT_1:def 7;

then A42: ex A13 being Subset of X st

( A3 = A13 & card A13 = k & S c= A13 ) by A35;

A43: B \ X1 c= B by XBOOLE_1:106;

then B1 in F " K by A18, A21, A33;

then A44: A1 in K by A36, FUNCT_1:def 7;

then A45: ex A11 being Subset of X st

( A1 = A11 & card A11 = k & S c= A11 ) by A35;

then A46: card A1 = (k - 1) + 1 ;

consider A2 being POINT of (G_ (k,X)) such that

A47: A2 = F . B2 ;

A48: B \ X2 c= B by XBOOLE_1:106;

then B2 in F " K by A18, A25, A26;

then A49: A2 in K by A47, FUNCT_1:def 7;

then consider L3a being LINE of (G_ (k,X)) such that

A50: {A1,A2} on L3a by A11, A44;

A51: card A1 = (k + 1) - 1 by A45;

A52: F is incidence_preserving by A3;

A53: card ((A1 /\ A2) /\ A3) c= card (A1 /\ A2) by CARD_1:11, XBOOLE_1:17;

consider L1 being LINE of (G_ (k,X)) such that

A54: L1 = F . L2 ;

B1 on L2 by A1, A12, A43, A33, A32, Th10;

then A55: A1 on L1 by A52, A36, A54;

then A56: A1 c= L1 by A1, A12, Th10;

L1 in the Lines of (G_ (k,X)) ;

then A57: ex l12 being Subset of X st

( L1 = l12 & card l12 = k + 1 ) by A14;

B3 on L2 by A1, A12, A40, A31, A32, Th10;

then A58: A3 on L1 by A52, A39, A54;

then A59: A3 c= L1 by A1, A12, Th10;

then A1 \/ A3 c= L1 by A56, XBOOLE_1:8;

then A60: card (A1 \/ A3) c= k + 1 by A57, CARD_1:11;

A61: ex A12 being Subset of X st

( A2 = A12 & card A12 = k & S c= A12 ) by A49, A35;

then A62: card A2 = (k - 1) + 1 ;

B2 on L2 by A1, A12, A48, A26, A32, Th10;

then A63: A2 on L1 by A52, A47, A54;

then A64: A2 c= L1 by A1, A12, Th10;

then A1 \/ A2 c= L1 by A56, XBOOLE_1:8;

then A65: card (A1 \/ A2) c= k + 1 by A57, CARD_1:11;

A66: ( the point-map of F is bijective & the Points of (G_ (k,X)) = dom the point-map of F ) by A3, FUNCT_2:52;

then A67: A1 <> A2 by A38, A33, A26, A36, A47, FUNCT_1:def 4;

then k + 1 c= card (A1 \/ A2) by A45, A61, Th1;

then card (A1 \/ A2) = (k - 1) + (2 * 1) by A65, XBOOLE_0:def 10;

then A68: card (A1 /\ A2) = (k + 1) - 2 by A4, A61, A46, Th2;

{A1,A2} on L1 by A55, A63, INCSP_1:1;

then A69: L1 = L3a by A67, A50, INCSP_1:def 10;

consider L3b being LINE of (G_ (k,X)) such that

A70: {A2,A3} on L3b by A11, A49, A41;

A1 <> A3 by A66, A38, A33, A31, A36, A39, FUNCT_1:def 4;

then k + 1 c= card (A1 \/ A3) by A45, A42, Th1;

then card (A1 \/ A3) = (k - 1) + (2 * 1) by A60, XBOOLE_0:def 10;

then A71: card (A1 /\ A3) = (k + 1) - 2 by A4, A42, A46, Th2;

A3 on L3b by A70, INCSP_1:1;

then A72: A3 c= L3b by A1, A12, Th10;

A2 on L3b by A70, INCSP_1:1;

then A73: A2 c= L3b by A1, A12, Th10;

L3b in the Lines of (G_ (k,X)) ;

then A74: ex l13b being Subset of X st

( L3b = l13b & card l13b = k + 1 ) by A14;

card (A1 /\ A2) in succ (k - 1) by A5, A67, A45, A61, Th1;

then card (A1 /\ A2) c= m by A24, ORDINAL1:22;

then A75: card ((A1 /\ A2) /\ A3) c= m by A53;

S c= A1 /\ A2 by A45, A61, XBOOLE_1:19;

then S c= (A1 /\ A2) /\ A3 by A42, XBOOLE_1:19;

then m c= card ((A1 /\ A2) /\ A3) by A34, A24, CARD_1:11;

then A76: k - 1 = card ((A1 /\ A2) /\ A3) by A24, A75, XBOOLE_0:def 10;

A1 on L3a by A50, INCSP_1:1;

then A77: A1 c= L3a by A1, A12, Th10;

A78: k - 1 <> (k + 1) - 3 ;

A2 \/ A3 c= L1 by A64, A59, XBOOLE_1:8;

then A79: card (A2 \/ A3) c= k + 1 by A57, CARD_1:11;

A80: A2 <> A3 by A66, A38, A26, A31, A47, A39, FUNCT_1:def 4;

then k + 1 c= card (A2 \/ A3) by A61, A42, Th1;

then card (A2 \/ A3) = (k - 1) + (2 * 1) by A79, XBOOLE_0:def 10;

then A81: card (A2 /\ A3) = (k + 1) - 2 by A4, A42, A62, Th2;

( 2 + 1 <= k + 1 & 2 <= k + 1 ) by A1, A15, XREAL_1:6, XXREAL_0:2;

then A82: card ((A1 \/ A2) \/ A3) = (k + 1) + 1 by A61, A42, A76, A68, A51, A81, A71, A78, Th7;

A83: L3a <> L3b

proof

{A2,A3} on L1
by A63, A58, INCSP_1:1;
assume
L3a = L3b
; :: thesis: contradiction

then A1 \/ A2 c= L3b by A77, A73, XBOOLE_1:8;

then (A1 \/ A2) \/ A3 c= L3b by A72, XBOOLE_1:8;

then Segm (k + 2) c= Segm (k + 1) by A82, A74, CARD_1:11;

then k + 2 <= k + 1 by NAT_1:39;

hence contradiction by XREAL_1:6; :: thesis: verum

end;then A1 \/ A2 c= L3b by A77, A73, XBOOLE_1:8;

then (A1 \/ A2) \/ A3 c= L3b by A72, XBOOLE_1:8;

then Segm (k + 2) c= Segm (k + 1) by A82, A74, CARD_1:11;

then k + 2 <= k + 1 by NAT_1:39;

hence contradiction by XREAL_1:6; :: thesis: verum

hence contradiction by A80, A70, A83, A69, INCSP_1:def 10; :: thesis: verum

proof

( F .: K is maximal_clique & F " K is maximal_clique )
by A3, A10, Th22;
A85:
k - 1 <> (k + 1) - 3
;

assume F .: K is TOP ; :: thesis: contradiction

then consider B being Subset of X such that

A86: ( card B = k + 1 & F .: K = { A where A is Subset of X : ( card A = k & A c= B ) } ) ;

B in the Lines of (G_ (k,X)) by A14, A86;

then consider L2 being LINE of (G_ (k,X)) such that

A87: B = L2 ;

the line-map of F is bijective by A3;

then the Lines of (G_ (k,X)) = rng the line-map of F by FUNCT_2:def 3;

then consider l1 being object such that

A88: l1 in dom the line-map of F and

A89: L2 = the line-map of F . l1 by FUNCT_1:def 3;

consider L1 being LINE of (G_ (k,X)) such that

A90: l1 = L1 by A88;

A91: L2 = F . L1 by A89, A90;

consider X1 being set such that

A92: ( X1 c= B & card X1 = 1 ) by A16, A86, CARD_FIL:36;

A93: B is finite by A86;

then A94: card (B \ X1) = (k + 1) - 1 by A86, A92, CARD_2:44;

then consider X2 being set such that

A95: X2 c= B \ X1 and

A96: card X2 = 1 by A8, CARD_FIL:36;

consider m being Nat such that

A97: m = k - 1 by A4;

card ((B \ X1) \ X2) = k - 1 by A93, A94, A95, A96, CARD_2:44;

then consider X3 being set such that

A98: X3 c= (B \ X1) \ X2 and

A99: card X3 = 1 by A6, CARD_FIL:36;

A100: X3 c= B \ (X2 \/ X1) by A98, XBOOLE_1:41;

then A101: card (B \ X3) = (k + 1) - 1 by A86, A93, A99, CARD_2:44, XBOOLE_1:106;

then B \ X3 in the Points of (G_ (k,X)) by A13;

then consider B3 being POINT of (G_ (k,X)) such that

A102: B \ X3 = B3 ;

L1 in the Lines of (G_ (k,X)) ;

then A103: ex l12 being Subset of X st

( L1 = l12 & card l12 = k + 1 ) by A14;

B \ X1 in the Points of (G_ (k,X)) by A13, A94;

then consider B1 being POINT of (G_ (k,X)) such that

A104: B \ X1 = B1 ;

A105: B \ X1 c= B by XBOOLE_1:106;

then A106: B1 on L2 by A1, A12, A104, A87, Th10;

consider S being Subset of X such that

A107: card S = k - 1 and

A108: K = { A where A is Subset of X : ( card A = k & S c= A ) } by A9;

A109: F is incidence_preserving by A3;

A110: B \ X3 c= B by XBOOLE_1:106;

then A111: B3 on L2 by A1, A12, A102, A87, Th10;

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

then A113: the Points of (G_ (k,X)) = rng the point-map of F by FUNCT_2:def 3;

then consider a3 being object such that

A114: a3 in dom the point-map of F and

A115: B3 = the point-map of F . a3 by FUNCT_1:def 3;

consider A3 being POINT of (G_ (k,X)) such that

A116: a3 = A3 by A114;

consider a1 being object such that

A117: a1 in dom the point-map of F and

A118: B1 = the point-map of F . a1 by A113, FUNCT_1:def 3;

consider A1 being POINT of (G_ (k,X)) such that

A119: a1 = A1 by A117;

B3 in F .: K by A86, A101, A110, A102;

then ex C3 being object st

( C3 in dom the point-map of F & C3 in K & B3 = the point-map of F . C3 ) by FUNCT_1:def 6;

then A120: A3 in K by A112, A114, A115, A116, FUNCT_1:def 4;

then A121: ex A13 being Subset of X st

( A3 = A13 & card A13 = k & S c= A13 ) by A108;

B1 in F .: K by A86, A94, A105, A104;

then ex C1 being object st

( C1 in dom the point-map of F & C1 in K & B1 = the point-map of F . C1 ) by FUNCT_1:def 6;

then A122: A1 in K by A112, A117, A118, A119, FUNCT_1:def 4;

then A123: ex A11 being Subset of X st

( A1 = A11 & card A11 = k & S c= A11 ) by A108;

then A124: card A1 = (k - 1) + 1 ;

A125: B1 = F . A1 by A118, A119;

then A1 on L1 by A109, A106, A91;

then A126: A1 c= L1 by A1, A12, Th10;

A127: B3 = F . A3 by A115, A116;

then A3 on L1 by A109, A111, A91;

then A128: A3 c= L1 by A1, A12, Th10;

then A1 \/ A3 c= L1 by A126, XBOOLE_1:8;

then A129: card (A1 \/ A3) c= k + 1 by A103, CARD_1:11;

A130: X3 c= (B \ X2) \ X1 by A100, XBOOLE_1:41;

A131: ( B \ X1 <> B \ X2 & B \ X2 <> B \ X3 & B \ X1 <> B \ X3 )

then card (A1 \/ A3) = (k - 1) + (2 * 1) by A129, XBOOLE_0:def 10;

then A132: card (A1 /\ A3) = (k + 1) - 2 by A4, A121, A124, Th2;

A133: card (B \ X2) = (k + 1) - 1 by A86, A93, A95, A96, CARD_2:44, XBOOLE_1:106;

then B \ X2 in the Points of (G_ (k,X)) by A13;

then consider B2 being POINT of (G_ (k,X)) such that

A134: B \ X2 = B2 ;

A135: B \ X2 c= B by XBOOLE_1:106;

then A136: B2 on L2 by A1, A12, A134, A87, Th10;

consider a2 being object such that

A137: a2 in dom the point-map of F and

A138: B2 = the point-map of F . a2 by A113, FUNCT_1:def 3;

consider A2 being POINT of (G_ (k,X)) such that

A139: a2 = A2 by A137;

B2 in F .: K by A86, A133, A135, A134;

then ex C2 being object st

( C2 in dom the point-map of F & C2 in K & B2 = the point-map of F . C2 ) by FUNCT_1:def 6;

then A140: A2 in K by A112, A137, A138, A139, FUNCT_1:def 4;

then A141: ex A12 being Subset of X st

( A2 = A12 & card A12 = k & S c= A12 ) by A108;

then A142: card A2 = (k - 1) + 1 ;

A143: B2 = F . A2 by A138, A139;

then A2 on L1 by A109, A136, A91;

then A144: A2 c= L1 by A1, A12, Th10;

then A1 \/ A2 c= L1 by A126, XBOOLE_1:8;

then A145: card (A1 \/ A2) c= k + 1 by A103, CARD_1:11;

k + 1 c= card (A1 \/ A2) by A131, A104, A134, A118, A138, A119, A139, A123, A141, Th1;

then card (A1 \/ A2) = (k - 1) + (2 * 1) by A145, XBOOLE_0:def 10;

then A146: card (A1 /\ A2) = (k + 1) - 2 by A4, A141, A124, Th2;

A147: A2 on L1 by A109, A136, A143, A91;

A2 \/ A3 c= L1 by A144, A128, XBOOLE_1:8;

then A148: card (A2 \/ A3) c= k + 1 by A103, CARD_1:11;

k + 1 c= card (A2 \/ A3) by A131, A134, A102, A138, A115, A139, A116, A141, A121, Th1;

then card (A2 \/ A3) = (k - 1) + (2 * 1) by A148, XBOOLE_0:def 10;

then A149: card (A2 /\ A3) = (k + 1) - 2 by A4, A121, A142, Th2;

A150: card A1 = (k + 1) - 1 by A123;

consider L3a being LINE of (G_ (k,X)) such that

A151: {A1,A2} on L3a by A11, A122, A140;

card (A1 /\ A2) in k by A131, A104, A134, A118, A138, A119, A139, A123, A141, Th1;

then A152: card (A1 /\ A2) c= m by A5, A97, ORDINAL1:22;

card ((A1 /\ A2) /\ A3) c= card (A1 /\ A2) by CARD_1:11, XBOOLE_1:17;

then A153: card ((A1 /\ A2) /\ A3) c= m by A152;

S c= A1 /\ A2 by A123, A141, XBOOLE_1:19;

then S c= (A1 /\ A2) /\ A3 by A121, XBOOLE_1:19;

then m c= card ((A1 /\ A2) /\ A3) by A107, A97, CARD_1:11;

then A154: k - 1 = card ((A1 /\ A2) /\ A3) by A97, A153, XBOOLE_0:def 10;

A1 on L3a by A151, INCSP_1:1;

then A155: A1 c= L3a by A1, A12, Th10;

consider L3b being LINE of (G_ (k,X)) such that

A156: {A2,A3} on L3b by A11, A140, A120;

A3 on L3b by A156, INCSP_1:1;

then A157: A3 c= L3b by A1, A12, Th10;

A2 on L3b by A156, INCSP_1:1;

then A158: A2 c= L3b by A1, A12, Th10;

L3b in the Lines of (G_ (k,X)) ;

then A159: ex l13b being Subset of X st

( L3b = l13b & card l13b = k + 1 ) by A14;

( 2 + 1 <= k + 1 & 2 <= k + 1 ) by A1, A15, XREAL_1:6, XXREAL_0:2;

then A160: card ((A1 \/ A2) \/ A3) = (k + 1) + 1 by A141, A121, A154, A146, A150, A149, A132, A85, Th7;

A161: L3a <> L3b

then {A1,A2} on L1 by A147, INCSP_1:1;

then A162: L1 = L3a by A131, A104, A134, A118, A138, A119, A139, A151, INCSP_1:def 10;

A3 on L1 by A109, A111, A127, A91;

then {A2,A3} on L1 by A147, INCSP_1:1;

hence contradiction by A131, A134, A102, A138, A115, A139, A116, A156, A161, A162, INCSP_1:def 10; :: thesis: verum

end;assume F .: K is TOP ; :: thesis: contradiction

then consider B being Subset of X such that

A86: ( card B = k + 1 & F .: K = { A where A is Subset of X : ( card A = k & A c= B ) } ) ;

B in the Lines of (G_ (k,X)) by A14, A86;

then consider L2 being LINE of (G_ (k,X)) such that

A87: B = L2 ;

the line-map of F is bijective by A3;

then the Lines of (G_ (k,X)) = rng the line-map of F by FUNCT_2:def 3;

then consider l1 being object such that

A88: l1 in dom the line-map of F and

A89: L2 = the line-map of F . l1 by FUNCT_1:def 3;

consider L1 being LINE of (G_ (k,X)) such that

A90: l1 = L1 by A88;

A91: L2 = F . L1 by A89, A90;

consider X1 being set such that

A92: ( X1 c= B & card X1 = 1 ) by A16, A86, CARD_FIL:36;

A93: B is finite by A86;

then A94: card (B \ X1) = (k + 1) - 1 by A86, A92, CARD_2:44;

then consider X2 being set such that

A95: X2 c= B \ X1 and

A96: card X2 = 1 by A8, CARD_FIL:36;

consider m being Nat such that

A97: m = k - 1 by A4;

card ((B \ X1) \ X2) = k - 1 by A93, A94, A95, A96, CARD_2:44;

then consider X3 being set such that

A98: X3 c= (B \ X1) \ X2 and

A99: card X3 = 1 by A6, CARD_FIL:36;

A100: X3 c= B \ (X2 \/ X1) by A98, XBOOLE_1:41;

then A101: card (B \ X3) = (k + 1) - 1 by A86, A93, A99, CARD_2:44, XBOOLE_1:106;

then B \ X3 in the Points of (G_ (k,X)) by A13;

then consider B3 being POINT of (G_ (k,X)) such that

A102: B \ X3 = B3 ;

L1 in the Lines of (G_ (k,X)) ;

then A103: ex l12 being Subset of X st

( L1 = l12 & card l12 = k + 1 ) by A14;

B \ X1 in the Points of (G_ (k,X)) by A13, A94;

then consider B1 being POINT of (G_ (k,X)) such that

A104: B \ X1 = B1 ;

A105: B \ X1 c= B by XBOOLE_1:106;

then A106: B1 on L2 by A1, A12, A104, A87, Th10;

consider S being Subset of X such that

A107: card S = k - 1 and

A108: K = { A where A is Subset of X : ( card A = k & S c= A ) } by A9;

A109: F is incidence_preserving by A3;

A110: B \ X3 c= B by XBOOLE_1:106;

then A111: B3 on L2 by A1, A12, A102, A87, Th10;

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

then A113: the Points of (G_ (k,X)) = rng the point-map of F by FUNCT_2:def 3;

then consider a3 being object such that

A114: a3 in dom the point-map of F and

A115: B3 = the point-map of F . a3 by FUNCT_1:def 3;

consider A3 being POINT of (G_ (k,X)) such that

A116: a3 = A3 by A114;

consider a1 being object such that

A117: a1 in dom the point-map of F and

A118: B1 = the point-map of F . a1 by A113, FUNCT_1:def 3;

consider A1 being POINT of (G_ (k,X)) such that

A119: a1 = A1 by A117;

B3 in F .: K by A86, A101, A110, A102;

then ex C3 being object st

( C3 in dom the point-map of F & C3 in K & B3 = the point-map of F . C3 ) by FUNCT_1:def 6;

then A120: A3 in K by A112, A114, A115, A116, FUNCT_1:def 4;

then A121: ex A13 being Subset of X st

( A3 = A13 & card A13 = k & S c= A13 ) by A108;

B1 in F .: K by A86, A94, A105, A104;

then ex C1 being object st

( C1 in dom the point-map of F & C1 in K & B1 = the point-map of F . C1 ) by FUNCT_1:def 6;

then A122: A1 in K by A112, A117, A118, A119, FUNCT_1:def 4;

then A123: ex A11 being Subset of X st

( A1 = A11 & card A11 = k & S c= A11 ) by A108;

then A124: card A1 = (k - 1) + 1 ;

A125: B1 = F . A1 by A118, A119;

then A1 on L1 by A109, A106, A91;

then A126: A1 c= L1 by A1, A12, Th10;

A127: B3 = F . A3 by A115, A116;

then A3 on L1 by A109, A111, A91;

then A128: A3 c= L1 by A1, A12, Th10;

then A1 \/ A3 c= L1 by A126, XBOOLE_1:8;

then A129: card (A1 \/ A3) c= k + 1 by A103, CARD_1:11;

A130: X3 c= (B \ X2) \ X1 by A100, XBOOLE_1:41;

A131: ( B \ X1 <> B \ X2 & B \ X2 <> B \ X3 & B \ X1 <> B \ X3 )

proof

then
k + 1 c= card (A1 \/ A3)
by A104, A102, A118, A115, A119, A116, A123, A121, Th1;
assume
( B \ X1 = B \ X2 or B \ X2 = B \ X3 or B \ X1 = B \ X3 )
; :: thesis: contradiction

then ( X2 = {} or X3 = {} or X3 = {} ) by A95, A98, A130, XBOOLE_1:38, XBOOLE_1:106;

hence contradiction by A96, A99; :: thesis: verum

end;then ( X2 = {} or X3 = {} or X3 = {} ) by A95, A98, A130, XBOOLE_1:38, XBOOLE_1:106;

hence contradiction by A96, A99; :: thesis: verum

then card (A1 \/ A3) = (k - 1) + (2 * 1) by A129, XBOOLE_0:def 10;

then A132: card (A1 /\ A3) = (k + 1) - 2 by A4, A121, A124, Th2;

A133: card (B \ X2) = (k + 1) - 1 by A86, A93, A95, A96, CARD_2:44, XBOOLE_1:106;

then B \ X2 in the Points of (G_ (k,X)) by A13;

then consider B2 being POINT of (G_ (k,X)) such that

A134: B \ X2 = B2 ;

A135: B \ X2 c= B by XBOOLE_1:106;

then A136: B2 on L2 by A1, A12, A134, A87, Th10;

consider a2 being object such that

A137: a2 in dom the point-map of F and

A138: B2 = the point-map of F . a2 by A113, FUNCT_1:def 3;

consider A2 being POINT of (G_ (k,X)) such that

A139: a2 = A2 by A137;

B2 in F .: K by A86, A133, A135, A134;

then ex C2 being object st

( C2 in dom the point-map of F & C2 in K & B2 = the point-map of F . C2 ) by FUNCT_1:def 6;

then A140: A2 in K by A112, A137, A138, A139, FUNCT_1:def 4;

then A141: ex A12 being Subset of X st

( A2 = A12 & card A12 = k & S c= A12 ) by A108;

then A142: card A2 = (k - 1) + 1 ;

A143: B2 = F . A2 by A138, A139;

then A2 on L1 by A109, A136, A91;

then A144: A2 c= L1 by A1, A12, Th10;

then A1 \/ A2 c= L1 by A126, XBOOLE_1:8;

then A145: card (A1 \/ A2) c= k + 1 by A103, CARD_1:11;

k + 1 c= card (A1 \/ A2) by A131, A104, A134, A118, A138, A119, A139, A123, A141, Th1;

then card (A1 \/ A2) = (k - 1) + (2 * 1) by A145, XBOOLE_0:def 10;

then A146: card (A1 /\ A2) = (k + 1) - 2 by A4, A141, A124, Th2;

A147: A2 on L1 by A109, A136, A143, A91;

A2 \/ A3 c= L1 by A144, A128, XBOOLE_1:8;

then A148: card (A2 \/ A3) c= k + 1 by A103, CARD_1:11;

k + 1 c= card (A2 \/ A3) by A131, A134, A102, A138, A115, A139, A116, A141, A121, Th1;

then card (A2 \/ A3) = (k - 1) + (2 * 1) by A148, XBOOLE_0:def 10;

then A149: card (A2 /\ A3) = (k + 1) - 2 by A4, A121, A142, Th2;

A150: card A1 = (k + 1) - 1 by A123;

consider L3a being LINE of (G_ (k,X)) such that

A151: {A1,A2} on L3a by A11, A122, A140;

card (A1 /\ A2) in k by A131, A104, A134, A118, A138, A119, A139, A123, A141, Th1;

then A152: card (A1 /\ A2) c= m by A5, A97, ORDINAL1:22;

card ((A1 /\ A2) /\ A3) c= card (A1 /\ A2) by CARD_1:11, XBOOLE_1:17;

then A153: card ((A1 /\ A2) /\ A3) c= m by A152;

S c= A1 /\ A2 by A123, A141, XBOOLE_1:19;

then S c= (A1 /\ A2) /\ A3 by A121, XBOOLE_1:19;

then m c= card ((A1 /\ A2) /\ A3) by A107, A97, CARD_1:11;

then A154: k - 1 = card ((A1 /\ A2) /\ A3) by A97, A153, XBOOLE_0:def 10;

A1 on L3a by A151, INCSP_1:1;

then A155: A1 c= L3a by A1, A12, Th10;

consider L3b being LINE of (G_ (k,X)) such that

A156: {A2,A3} on L3b by A11, A140, A120;

A3 on L3b by A156, INCSP_1:1;

then A157: A3 c= L3b by A1, A12, Th10;

A2 on L3b by A156, INCSP_1:1;

then A158: A2 c= L3b by A1, A12, Th10;

L3b in the Lines of (G_ (k,X)) ;

then A159: ex l13b being Subset of X st

( L3b = l13b & card l13b = k + 1 ) by A14;

( 2 + 1 <= k + 1 & 2 <= k + 1 ) by A1, A15, XREAL_1:6, XXREAL_0:2;

then A160: card ((A1 \/ A2) \/ A3) = (k + 1) + 1 by A141, A121, A154, A146, A150, A149, A132, A85, Th7;

A161: L3a <> L3b

proof

A1 on L1
by A109, A106, A125, A91;
assume
L3a = L3b
; :: thesis: contradiction

then A1 \/ A2 c= L3b by A155, A158, XBOOLE_1:8;

then (A1 \/ A2) \/ A3 c= L3b by A157, XBOOLE_1:8;

then Segm (k + 2) c= Segm (k + 1) by A160, A159, CARD_1:11;

then k + 2 <= k + 1 by NAT_1:39;

hence contradiction by XREAL_1:6; :: thesis: verum

end;then A1 \/ A2 c= L3b by A155, A158, XBOOLE_1:8;

then (A1 \/ A2) \/ A3 c= L3b by A157, XBOOLE_1:8;

then Segm (k + 2) c= Segm (k + 1) by A160, A159, CARD_1:11;

then k + 2 <= k + 1 by NAT_1:39;

hence contradiction by XREAL_1:6; :: thesis: verum

then {A1,A2} on L1 by A147, INCSP_1:1;

then A162: L1 = L3a by A131, A104, A134, A118, A138, A119, A139, A151, INCSP_1:def 10;

A3 on L1 by A109, A111, A127, A91;

then {A2,A3} on L1 by A147, INCSP_1:1;

hence contradiction by A131, A134, A102, A138, A115, A139, A116, A156, A161, A162, INCSP_1:def 10; :: thesis: verum

hence ( F .: K is STAR & F " K is STAR ) by A1, A2, A84, A17, Th15; :: thesis: verum