begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
for
X,
Y,
Z being
set st
X \ Y = X \ Z &
Y c= X &
Z c= X holds
Y = Z
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
begin
:: deftheorem Def1 defines G_ COMBGRAS:def 1 :
theorem Th10:
theorem Th11:
theorem Th12:
for
k being
Element of
NAT for
X being non
empty set st
0 < k &
k + 1
c= card X holds
for
A1,
A2,
A3,
A4,
A5,
A6 being
POINT of
(G_ k,X) for
L1,
L2,
L3,
L4 being
LINE of
(G_ k,X) st
A1 on L1 &
A2 on L1 &
A3 on L2 &
A4 on L2 &
A5 on L1 &
A5 on L2 &
A1 on L3 &
A3 on L3 &
A2 on L4 &
A4 on L4 & not
A5 on L3 & not
A5 on L4 &
L1 <> L2 &
L3 <> L4 holds
ex
A6 being
POINT of
(G_ k,X) st
(
A6 on L3 &
A6 on L4 &
A6 = (A1 /\ A2) \/ (A3 /\ A4) )
theorem
:: deftheorem Def2 defines clique COMBGRAS:def 2 :
:: deftheorem Def3 defines maximal_clique COMBGRAS:def 3 :
:: deftheorem Def4 defines STAR COMBGRAS:def 4 :
:: deftheorem Def5 defines TOP COMBGRAS:def 5 :
theorem Th14:
theorem Th15:
begin
:: deftheorem defines . COMBGRAS:def 6 :
:: deftheorem defines . COMBGRAS:def 7 :
theorem Th16:
:: deftheorem Def8 defines incidence_preserving COMBGRAS:def 8 :
theorem
:: deftheorem Def9 defines automorphism COMBGRAS:def 9 :
:: deftheorem defines .: COMBGRAS:def 10 :
:: deftheorem defines " COMBGRAS:def 11 :
:: deftheorem defines ^^ COMBGRAS:def 12 :
:: deftheorem Def13 defines ^^ COMBGRAS:def 13 :
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
definition
let k be
Element of
NAT ;
let X be non
empty set ;
assume A1:
(
0 < k &
k + 1
c= card X )
;
let s be
Permutation of
X;
func incprojmap k,
s -> strict IncProjMap of
G_ k,
X,
G_ k,
X means :
Def14:
( ( for
A being
POINT of
(G_ k,X) holds
it . A = s .: A ) & ( for
L being
LINE of
(G_ k,X) holds
it . L = s .: L ) );
existence
ex b1 being strict IncProjMap of G_ k,X, G_ k,X st
( ( for A being POINT of (G_ k,X) holds b1 . A = s .: A ) & ( for L being LINE of (G_ k,X) holds b1 . L = s .: L ) )
uniqueness
for b1, b2 being strict IncProjMap of G_ k,X, G_ k,X st ( for A being POINT of (G_ k,X) holds b1 . A = s .: A ) & ( for L being LINE of (G_ k,X) holds b1 . L = s .: L ) & ( for A being POINT of (G_ k,X) holds b2 . A = s .: A ) & ( for L being LINE of (G_ k,X) holds b2 . L = s .: L ) holds
b1 = b2
end;
:: deftheorem Def14 defines incprojmap COMBGRAS:def 14 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
for
k being
Element of
NAT for
X being non
empty set st
0 < k &
k + 3
c= card X holds
for
F being
IncProjMap of
G_ (k + 1),
X,
G_ (k + 1),
X st
F is
automorphism holds
for
H being
IncProjMap of
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
theorem Th33:
theorem Th34:
theorem