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 of 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 of 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 A1:
( 2 <= k & k + 2 c= card X )
; :: thesis: for F being IncProjMap of 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 of 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 A2:
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 )
let K be Subset of the Points of (G_ k,X); :: thesis: ( K is STAR implies ( F .: K is STAR & F " K is STAR ) )
A3:
( k + 1 <= k + 2 & 1 <= k & k + 0 <= k + 1 & 0 <= 1 )
by A1, XREAL_1:9, XXREAL_0:2;
then
( - 2 < 0 & k + 1 c= k + 2 & k + 0 <= k + 1 )
by NAT_1:40;
then A4:
( 2 - 2 < k & k + 1 c= card X & 2 - 1 <= k - 1 & 1 <= k + 1 & k - 1 is Element of NAT & k - 2 is Element of NAT )
by A1, A3, NAT_1:21, XBOOLE_1:1, XREAL_1:11, XXREAL_0:2;
then A5:
( 1 c= k + 1 & 1 c= k & 1 c= k - 1 & card (k + 1) = k + 1 & card 1 = 1 & card k = k & succ (k - 1) = (k - 1) + 1 & succ 2 = 2 + 1 )
by A3, CARD_1:def 5, NAT_1:39, NAT_1:40;
A6:
the Points of (G_ k,X) = { A where A is Subset of X : card A = k }
by A4, Def1;
A7:
the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 }
by A4, Def1;
assume A8:
K is STAR
; :: thesis: ( F .: K is STAR & F " K is STAR )
then
K is maximal_clique
by A1, Th14;
then A9:
( F .: K is maximal_clique & F " K is maximal_clique & K is clique )
by A2, Def3, Th22;
A10:
not F .: K is TOP
proof
assume
F .: K is
TOP
;
:: thesis: contradiction
then consider B being
Subset of
X such that A11:
(
card B = k + 1 &
F .: K = { A where A is Subset of X : ( card A = k & A c= B ) } )
by Def5;
consider X1 being
set such that A12:
(
X1 c= B &
card X1 = 1 )
by A5, A11, CARD_FIL:36;
A13:
(
X1 is
finite &
B is
finite )
by A11, A12;
then A14:
card (B \ X1) = (k + 1) - 1
by A11, A12, CARD_2:63;
then consider X2 being
set such that A15:
(
X2 c= B \ X1 &
card X2 = 1 )
by A5, CARD_FIL:36;
(
X2 is
finite &
B \ X1 is
finite )
by A14, A15;
then
card ((B \ X1) \ X2) = k - 1
by A14, A15, CARD_2:63;
then consider X3 being
set such that A17:
(
X3 c= (B \ X1) \ X2 &
card X3 = 1 )
by A5, CARD_FIL:36;
(
X3 c= B \ (X2 \/ X1) & the
point-map of
F is
bijective & the
line-map of
F is
bijective )
by A2, A17, Def9, XBOOLE_1:41;
then A18:
(
X3 c= B &
X2 c= B &
X3 is
finite &
X3 c= (B \ X2) \ X1 & the
point-map of
F is
onto & the
line-map of
F is
onto &
F is
incidence_preserving & the
point-map of
F is
one-to-one )
by A2, A15, A17, Def9, XBOOLE_1:41, XBOOLE_1:106;
then A19:
(
card (B \ X2) = (k + 1) - 1 &
card (B \ X3) = (k + 1) - 1 &
B \ X1 c= X &
B \ X2 c= X &
B \ X3 c= X &
X3 c= B \ X2 &
X3 c= B \ X1 &
X1 misses X2 &
X2 misses X3 &
X1 misses X3 &
B \ X1 c= B &
B \ X2 c= B &
B \ X3 c= B & the
Points of
(G_ k,X) = rng the
point-map of
F & the
Lines of
(G_ k,X) = rng the
line-map of
F & the
Points of
(G_ k,X) = dom the
point-map of
F & the
Lines of
(G_ k,X) = dom the
line-map of
F )
by A11, A13, A15, A17, CARD_2:63, FUNCT_2:67, FUNCT_2:def 3, XBOOLE_1:106;
then A20:
(
B \ X1 in the
Points of
(G_ k,X) &
B \ X2 in the
Points of
(G_ k,X) &
B \ X3 in the
Points of
(G_ k,X) &
B in the
Lines of
(G_ k,X) )
by A6, A7, A11, A14;
A21:
(
B \ X1 <> B \ X2 &
B \ X2 <> B \ X3 &
B \ X1 <> B \ X3 )
consider B1 being
POINT of
(G_ k,X) such that A22:
B \ X1 = B1
by A20;
consider B2 being
POINT of
(G_ k,X) such that A23:
B \ X2 = B2
by A20;
consider B3 being
POINT of
(G_ k,X) such that A24:
B \ X3 = B3
by A20;
consider L2 being
LINE of
(G_ k,X) such that A25:
B = L2
by A20;
A26:
(
B1 on L2 &
B2 on L2 &
B3 on L2 &
B1 in rng the
point-map of
F &
B2 in rng the
point-map of
F &
B3 in rng the
point-map of
F &
L2 in rng the
line-map of
F )
by A4, A19, A22, A23, A24, A25, Th10;
consider a1 being
set such that A27:
(
a1 in dom the
point-map of
F &
B1 = the
point-map of
F . a1 )
by A19, FUNCT_1:def 5;
consider a2 being
set such that A28:
(
a2 in dom the
point-map of
F &
B2 = the
point-map of
F . a2 )
by A19, FUNCT_1:def 5;
consider a3 being
set such that A29:
(
a3 in dom the
point-map of
F &
B3 = the
point-map of
F . a3 )
by A19, FUNCT_1:def 5;
consider l1 being
set such that A30:
(
l1 in dom the
line-map of
F &
L2 = the
line-map of
F . l1 )
by A19, FUNCT_1:def 5;
consider A1 being
POINT of
(G_ k,X) such that A31:
a1 = A1
by A27;
consider A2 being
POINT of
(G_ k,X) such that A32:
a2 = A2
by A28;
consider A3 being
POINT of
(G_ k,X) such that A33:
a3 = A3
by A29;
consider L1 being
LINE of
(G_ k,X) such that A34:
l1 = L1
by A30;
A35:
(
B1 = F . A1 &
B2 = F . A2 &
B3 = F . A3 &
L2 = F . L1 )
by A27, A28, A29, A30, A31, A32, A33, A34;
then
(
A1 on L1 &
A2 on L1 &
A3 on L1 )
by A18, A26, Def8;
then A36:
(
A1 c= L1 &
A2 c= L1 &
A3 c= L1 &
A1 <> A2 &
A2 <> A3 &
A1 <> A3 &
B1 in F .: K &
B2 in F .: K &
B3 in F .: K )
by A4, A11, A14, A19, A21, A22, A23, A24, A27, A28, A29, A31, A32, A33, Th10;
then consider C1 being
set such that A37:
(
C1 in dom the
point-map of
F &
C1 in K &
B1 = the
point-map of
F . C1 )
by FUNCT_1:def 12;
consider C2 being
set such that A38:
(
C2 in dom the
point-map of
F &
C2 in K &
B2 = the
point-map of
F . C2 )
by A36, FUNCT_1:def 12;
consider C3 being
set such that A39:
(
C3 in dom the
point-map of
F &
C3 in K &
B3 = the
point-map of
F . C3 )
by A36, FUNCT_1:def 12;
A40:
(
A1 in K &
A2 in K &
A3 in K )
by A18, A27, A28, A29, A31, A32, A33, A37, A38, A39, FUNCT_1:def 8;
then consider L3a being
LINE of
(G_ k,X) such that A41:
{A1,A2} on L3a
by A9, Def2;
consider L3b being
LINE of
(G_ k,X) such that A42:
{A2,A3} on L3b
by A9, A40, Def2;
consider S being
Subset of
X such that A43:
(
card S = k - 1 &
K = { A where A is Subset of X : ( card A = k & S c= A ) } )
by A8, Def4;
consider A11 being
Subset of
X such that A44:
(
A1 = A11 &
card A11 = k &
S c= A11 )
by A40, A43;
consider A12 being
Subset of
X such that A45:
(
A2 = A12 &
card A12 = k &
S c= A12 )
by A40, A43;
consider A13 being
Subset of
X such that A46:
(
A3 = A13 &
card A13 = k &
S c= A13 )
by A40, A43;
consider m being
Nat such that A47:
m = k - 1
by A4;
L1 in the
Lines of
(G_ k,X)
;
then consider l12 being
Subset of
X such that A48:
(
L1 = l12 &
card l12 = k + 1 )
by A7;
(
S c= A1 /\ A2 &
card (A1 /\ A2) in k &
A1 \/ A2 c= L1 &
A1 \/ A3 c= L1 &
A2 \/ A3 c= L1 & 2
c= k )
by A1, A36, A44, A45, Th1, NAT_1:40, XBOOLE_1:8, XBOOLE_1:19;
then
(
S c= (A1 /\ A2) /\ A3 &
card (A1 /\ A2) in succ (k - 1) &
(A1 /\ A2) /\ A3 c= A1 /\ A2 &
card (A1 \/ A2) c= k + 1 &
card (A1 \/ A3) c= k + 1 &
card (A2 \/ A3) c= k + 1 &
k + 1
c= card (A1 \/ A2) &
k + 1
c= card (A1 \/ A3) &
k + 1
c= card (A2 \/ A3) & 2
in succ k )
by A5, A36, A44, A45, A46, A48, Th1, CARD_1:27, ORDINAL1:34, XBOOLE_1:17, XBOOLE_1:19;
then A49:
(
m c= card ((A1 /\ A2) /\ A3) &
card (A1 /\ A2) c= m &
card (A1 \/ A2) = k + 1 &
card (A2 \/ A3) = k + 1 &
card (A1 \/ A3) = k + 1 &
card ((A1 /\ A2) /\ A3) c= card (A1 /\ A2) & ( 2
in k or
k = 2 ) )
by A43, A47, CARD_1:27, ORDINAL1:13, ORDINAL1:34, XBOOLE_0:def 10;
then
(
card ((A1 /\ A2) /\ A3) c= m & ( 3
c= k or
k = 2 ) )
by A5, ORDINAL1:33, XBOOLE_1:1;
then A50:
(
k - 1
= card ((A1 /\ A2) /\ A3) &
card (A1 \/ A2) = (k - 1) + (2 * 1) &
card A1 = (k - 1) + 1 &
card (A2 \/ A3) = (k - 1) + (2 * 1) &
card (A1 \/ A3) = (k - 1) + (2 * 1) &
card A2 = (k - 1) + 1 &
card A3 = (k - 1) + 1 )
by A44, A45, A46, A47, A49, XBOOLE_0:def 10;
then
(
card (A1 /\ A2) = (k + 1) - 2 &
card A1 = (k + 1) - 1 &
card (A2 /\ A3) = (k + 1) - 2 &
card (A1 /\ A3) = (k + 1) - 2 &
card A2 = (k + 1) - 1 &
card A3 = (k + 1) - 1 & 2
+ 1
<= k + 1 & 2
<= k + 1 &
k - 1
<> (k + 1) - 3 &
A1 on L3a &
A2 on L3b &
A3 on L3b )
by A1, A3, A4, A41, A42, Th2, INCSP_1:11, XREAL_1:8, XXREAL_0:2;
then A51:
(
card ((A1 \/ A2) \/ A3) = (k + 1) + 1 &
card ((A1 /\ A2) /\ A3) = (k + 1) - 2 &
A1 c= L3a &
A2 c= L3b &
A3 c= L3b )
by A4, A50, Th7, Th10;
L3b in the
Lines of
(G_ k,X)
;
then consider l13b being
Subset of
X such that A52:
(
L3b = l13b &
card l13b = k + 1 )
by A7;
A53:
L3a <> L3b
(
A1 on L1 &
A2 on L1 &
A3 on L1 )
by A18, A26, A35, Def8;
then
(
{A1,A2} on L1 &
{A2,A3} on L1 )
by INCSP_1:11;
then
(
L1 = L3a &
L1 = L3b )
by A21, A22, A23, A24, A27, A28, A29, A31, A32, A33, A41, A42, INCSP_1:def 10;
hence
contradiction
by A53;
:: thesis: verum
end;
not F " K is TOP
proof
assume
F " K is
TOP
;
:: thesis: contradiction
then consider B being
Subset of
X such that A54:
(
card B = k + 1 &
F " K = { A where A is Subset of X : ( card A = k & A c= B ) } )
by Def5;
consider X1 being
set such that A55:
(
X1 c= B &
card X1 = 1 )
by A5, A54, CARD_FIL:36;
A56:
(
X1 is
finite &
B is
finite )
by A54, A55;
then A57:
card (B \ X1) = (k + 1) - 1
by A54, A55, CARD_2:63;
then consider X2 being
set such that A58:
(
X2 c= B \ X1 &
card X2 = 1 )
by A5, CARD_FIL:36;
(
X2 is
finite &
B \ X1 is
finite )
by A57, A58;
then
card ((B \ X1) \ X2) = k - 1
by A57, A58, CARD_2:63;
then consider X3 being
set such that A60:
(
X3 c= (B \ X1) \ X2 &
card X3 = 1 )
by A5, CARD_FIL:36;
(
X3 c= B \ (X2 \/ X1) & the
point-map of
F is
bijective & the
line-map of
F is
bijective )
by A2, A60, Def9, XBOOLE_1:41;
then A61:
(
X3 c= B &
X2 c= B &
X3 is
finite &
X3 c= (B \ X2) \ X1 & the
point-map of
F is
onto & the
line-map of
F is
onto &
F is
incidence_preserving & the
point-map of
F is
one-to-one & the
point-map of
F is
Function-like )
by A2, A58, A60, Def9, XBOOLE_1:41, XBOOLE_1:106;
then A62:
(
card (B \ X2) = (k + 1) - 1 &
card (B \ X3) = (k + 1) - 1 &
B \ X1 c= X &
B \ X2 c= X &
B \ X3 c= X &
X3 c= B \ X2 &
X3 c= B \ X1 &
X1 misses X2 &
X2 misses X3 &
X1 misses X3 &
B \ X1 c= B &
B \ X2 c= B &
B \ X3 c= B & the
Points of
(G_ k,X) = rng the
point-map of
F & the
Lines of
(G_ k,X) = rng the
line-map of
F & the
Points of
(G_ k,X) = dom the
point-map of
F & the
Lines of
(G_ k,X) = dom the
line-map of
F )
by A54, A56, A58, A60, CARD_2:63, FUNCT_2:67, FUNCT_2:def 3, XBOOLE_1:106;
then A63:
(
B \ X1 in the
Points of
(G_ k,X) &
B \ X2 in the
Points of
(G_ k,X) &
B \ X3 in the
Points of
(G_ k,X) &
B in the
Lines of
(G_ k,X) )
by A6, A7, A54, A57;
A64:
(
B \ X1 <> B \ X2 &
B \ X2 <> B \ X3 &
B \ X1 <> B \ X3 )
consider B1 being
POINT of
(G_ k,X) such that A65:
B \ X1 = B1
by A63;
consider B2 being
POINT of
(G_ k,X) such that A66:
B \ X2 = B2
by A63;
consider B3 being
POINT of
(G_ k,X) such that A67:
B \ X3 = B3
by A63;
consider L2 being
LINE of
(G_ k,X) such that A68:
B = L2
by A63;
A69:
(
B1 on L2 &
B2 on L2 &
B3 on L2 &
B1 in dom the
point-map of
F &
B2 in dom the
point-map of
F &
B3 in dom the
point-map of
F &
F . B2 in the
Points of
(G_ k,X) &
L2 in dom the
line-map of
F &
F . B1 in the
Points of
(G_ k,X) &
F . B3 in the
Points of
(G_ k,X) &
F . L2 in the
Lines of
(G_ k,X) )
by A4, A62, A65, A66, A67, A68, Th10;
consider A1 being
POINT of
(G_ k,X) such that A70:
A1 = F . B1
;
consider A2 being
POINT of
(G_ k,X) such that A71:
A2 = F . B2
;
consider A3 being
POINT of
(G_ k,X) such that A72:
A3 = F . B3
;
consider L1 being
LINE of
(G_ k,X) such that A73:
L1 = F . L2
;
A74:
(
A1 on L1 &
A2 on L1 &
A3 on L1 )
by A61, A69, A70, A71, A72, A73, Def8;
then A75:
(
A1 c= L1 &
A2 c= L1 &
A3 c= L1 &
B1 in F " K &
A1 <> A2 &
A2 <> A3 &
A1 <> A3 &
B2 in F " K &
B3 in F " K )
by A4, A54, A57, A61, A62, A64, A65, A66, A67, A70, A71, A72, Th10, FUNCT_1:def 8;
then A76:
(
A1 in K &
A2 in K &
A3 in K )
by A70, A71, A72, FUNCT_1:def 13;
then consider L3a being
LINE of
(G_ k,X) such that A77:
{A1,A2} on L3a
by A9, Def2;
consider L3b being
LINE of
(G_ k,X) such that A78:
{A2,A3} on L3b
by A9, A76, Def2;
consider S being
Subset of
X such that A79:
(
card S = k - 1 &
K = { A where A is Subset of X : ( card A = k & S c= A ) } )
by A8, Def4;
consider A11 being
Subset of
X such that A80:
(
A1 = A11 &
card A11 = k &
S c= A11 )
by A76, A79;
consider A12 being
Subset of
X such that A81:
(
A2 = A12 &
card A12 = k &
S c= A12 )
by A76, A79;
consider A13 being
Subset of
X such that A82:
(
A3 = A13 &
card A13 = k &
S c= A13 )
by A76, A79;
consider m being
Nat such that A83:
m = k - 1
by A4;
L1 in the
Lines of
(G_ k,X)
;
then consider l12 being
Subset of
X such that A84:
(
L1 = l12 &
card l12 = k + 1 )
by A7;
(
S c= A1 /\ A2 &
card (A1 /\ A2) in k &
A1 \/ A2 c= L1 &
A1 \/ A3 c= L1 &
A2 \/ A3 c= L1 & 2
c= k )
by A1, A75, A80, A81, Th1, NAT_1:40, XBOOLE_1:8, XBOOLE_1:19;
then
(
S c= (A1 /\ A2) /\ A3 &
card (A1 /\ A2) in succ (k - 1) &
(A1 /\ A2) /\ A3 c= A1 /\ A2 &
card (A1 \/ A2) c= k + 1 &
card (A1 \/ A3) c= k + 1 &
card (A2 \/ A3) c= k + 1 &
k + 1
c= card (A1 \/ A2) &
k + 1
c= card (A1 \/ A3) &
k + 1
c= card (A2 \/ A3) & 2
in succ k )
by A5, A75, A80, A81, A82, A84, Th1, CARD_1:27, ORDINAL1:34, XBOOLE_1:17, XBOOLE_1:19;
then A85:
(
m c= card ((A1 /\ A2) /\ A3) &
card (A1 /\ A2) c= m &
card (A1 \/ A2) = k + 1 &
card (A2 \/ A3) = k + 1 &
card (A1 \/ A3) = k + 1 &
card ((A1 /\ A2) /\ A3) c= card (A1 /\ A2) & ( 2
in k or
k = 2 ) )
by A79, A83, CARD_1:27, ORDINAL1:13, ORDINAL1:34, XBOOLE_0:def 10;
then
(
card ((A1 /\ A2) /\ A3) c= m & ( 3
c= k or
k = 2 ) )
by A5, ORDINAL1:33, XBOOLE_1:1;
then A86:
(
k - 1
= card ((A1 /\ A2) /\ A3) &
card (A1 \/ A2) = (k - 1) + (2 * 1) &
card A1 = (k - 1) + 1 &
card (A2 \/ A3) = (k - 1) + (2 * 1) &
card (A1 \/ A3) = (k - 1) + (2 * 1) &
card A2 = (k - 1) + 1 &
card A3 = (k - 1) + 1 )
by A80, A81, A82, A83, A85, XBOOLE_0:def 10;
then
(
card (A1 /\ A2) = (k + 1) - 2 &
card A1 = (k + 1) - 1 &
card (A2 /\ A3) = (k + 1) - 2 &
card (A1 /\ A3) = (k + 1) - 2 &
card A2 = (k + 1) - 1 &
card A3 = (k + 1) - 1 & 2
+ 1
<= k + 1 & 2
<= k + 1 &
k - 1
<> (k + 1) - 3 &
A1 on L3a &
A2 on L3b &
A3 on L3b )
by A1, A3, A4, A77, A78, Th2, INCSP_1:11, XREAL_1:8, XXREAL_0:2;
then A87:
(
card ((A1 \/ A2) \/ A3) = (k + 1) + 1 &
card ((A1 /\ A2) /\ A3) = (k + 1) - 2 &
A1 c= L3a &
A2 c= L3b &
A3 c= L3b )
by A4, A86, Th7, Th10;
L3b in the
Lines of
(G_ k,X)
;
then consider l13b being
Subset of
X such that A88:
(
L3b = l13b &
card l13b = k + 1 )
by A7;
A89:
L3a <> L3b
(
{A1,A2} on L1 &
{A2,A3} on L1 )
by A74, INCSP_1:11;
then
(
L1 = L3a &
L1 = L3b )
by A75, A77, A78, INCSP_1:def 10;
hence
contradiction
by A89;
:: thesis: verum
end;
hence
( F .: K is STAR & F " K is STAR )
by A1, A9, A10, Th15; :: thesis: verum