let k be Element of NAT ; 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 ; ( 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
; 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); ( 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
; 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)); ( K is STAR implies ( F .: K is STAR & F " K is STAR ) )
assume A9:
K is STAR
; ( 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
assume
F " K is
TOP
;
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 )
consider A3 being
POINT of
(G_ (k,X)) such that 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
{A2,A3} on L1
by A63, A58, INCSP_1:1;
hence
contradiction
by A80, A70, A83, A69, INCSP_1:def 10;
verum
end;
A84:
not F .: K is TOP
proof
A85:
k - 1
<> (k + 1) - 3
;
assume
F .: K is
TOP
;
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
k + 1
c= card (A1 \/ A3)
by A104, A102, A118, A115, A119, A116, A123, A121, Th1;
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
A1 on L1
by A109, A106, A125, A91;
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;
verum
end;
( F .: K is maximal_clique & F " K is maximal_clique )
by A3, A10, Th22;
hence
( F .: K is STAR & F " K is STAR )
by A1, A2, A84, A17, Th15; verum