:: by Andrzej Owsiejczuk

::

:: Received April 16, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

theorem Th1: :: COMBGRAS:1

for n being Nat

for a, b being set st a <> b & card a = n & card b = n holds

( card (a /\ b) in n & n + 1 c= card (a \/ b) )

for a, b being set st a <> b & card a = n & card b = n holds

( card (a /\ b) in n & n + 1 c= card (a \/ b) )

proof end;

theorem Th2: :: COMBGRAS:2

for k, n being Nat

for a, b being set st card a = n + k & card b = n + k holds

( card (a /\ b) = n iff card (a \/ b) = n + (2 * k) )

for a, b being set st card a = n + k & card b = n + k holds

( card (a /\ b) = n iff card (a \/ b) = n + (2 * k) )

proof end;

theorem Th3: :: COMBGRAS:3

for X, Y being set holds

( card X c= card Y iff ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y ) )

( card X c= card Y iff ex f being Function st

( f is one-to-one & X c= dom f & f .: X c= Y ) )

proof end;

theorem Th6: :: COMBGRAS:6

for X being set

for Y being non empty set

for p being Function of X,Y st p is one-to-one holds

for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

for Y being non empty set

for p being Function of X,Y st p is one-to-one holds

for x1, x2 being Subset of X st x1 <> x2 holds

p .: x1 <> p .: x2

proof end;

theorem Th7: :: COMBGRAS:7

for n being Nat

for a, b, c being set st card a = n - 1 & card b = n - 1 & card c = n - 1 & card (a /\ b) = n - 2 & card (a /\ c) = n - 2 & card (b /\ c) = n - 2 & 2 <= n holds

( ( not 3 <= n or ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) or ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) ) & ( n = 2 implies ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) ) )

for a, b, c being set st card a = n - 1 & card b = n - 1 & card c = n - 1 & card (a /\ b) = n - 2 & card (a /\ c) = n - 2 & card (b /\ c) = n - 2 & 2 <= n holds

( ( not 3 <= n or ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) or ( card ((a /\ b) /\ c) = n - 3 & card ((a \/ b) \/ c) = n ) ) & ( n = 2 implies ( card ((a /\ b) /\ c) = n - 2 & card ((a \/ b) \/ c) = n + 1 ) ) )

proof end;

theorem :: COMBGRAS:8

for P1, P2 being IncProjStr st IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) holds

for A1 being POINT of P1

for A2 being POINT of P2 st A1 = A2 holds

for L1 being LINE of P1

for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds

A2 on L2 ;

for A1 being POINT of P1

for A2 being POINT of P2 st A1 = A2 holds

for L1 being LINE of P1

for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds

A2 on L2 ;

theorem Th9: :: COMBGRAS:9

for P1, P2 being IncProjStr st IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) holds

for A1 being Subset of the Points of P1

for A2 being Subset of the Points of P2 st A1 = A2 holds

for L1 being LINE of P1

for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds

A2 on L2

for A1 being Subset of the Points of P1

for A2 being Subset of the Points of P2 st A1 = A2 holds

for L1 being LINE of P1

for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds

A2 on L2

proof end;

registration

existence

ex b_{1} being IncProjStr st

( b_{1} is with_non-trivial_lines & b_{1} is linear & b_{1} is up-2-rank & b_{1} is strict )

end;
ex b

( b

proof end;

definition

let k be Nat;

let X be non empty set ;

assume that

A1: 0 < k and

A2: k + 1 c= card X ;

ex b_{1} being strict PartialLinearSpace st

( the Points of b_{1} = { A where A is Subset of X : card A = k } & the Lines of b_{1} = { L where L is Subset of X : card L = k + 1 } & the Inc of b_{1} = (RelIncl (bool X)) /\ [: the Points of b_{1}, the Lines of b_{1}:] )

for b_{1}, b_{2} being strict PartialLinearSpace st the Points of b_{1} = { A where A is Subset of X : card A = k } & the Lines of b_{1} = { L where L is Subset of X : card L = k + 1 } & the Inc of b_{1} = (RelIncl (bool X)) /\ [: the Points of b_{1}, the Lines of b_{1}:] & the Points of b_{2} = { A where A is Subset of X : card A = k } & the Lines of b_{2} = { L where L is Subset of X : card L = k + 1 } & the Inc of b_{2} = (RelIncl (bool X)) /\ [: the Points of b_{2}, the Lines of b_{2}:] holds

b_{1} = b_{2}
;

end;
let X be non empty set ;

assume that

A1: 0 < k and

A2: k + 1 c= card X ;

func G_ (k,X) -> strict PartialLinearSpace means :Def1: :: COMBGRAS:def 1

( the Points of it = { A where A is Subset of X : card A = k } & the Lines of it = { L where L is Subset of X : card L = k + 1 } & the Inc of it = (RelIncl (bool X)) /\ [: the Points of it, the Lines of it:] );

existence ( the Points of it = { A where A is Subset of X : card A = k } & the Lines of it = { L where L is Subset of X : card L = k + 1 } & the Inc of it = (RelIncl (bool X)) /\ [: the Points of it, the Lines of it:] );

ex b

( the Points of b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines G_ COMBGRAS:def 1 :

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for b_{3} being strict PartialLinearSpace holds

( b_{3} = G_ (k,X) iff ( the Points of b_{3} = { A where A is Subset of X : card A = k } & the Lines of b_{3} = { L where L is Subset of X : card L = k + 1 } & the Inc of b_{3} = (RelIncl (bool X)) /\ [: the Points of b_{3}, the Lines of b_{3}:] ) );

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for b

( b

theorem Th10: :: COMBGRAS:10

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for A being POINT of (G_ (k,X))

for L being LINE of (G_ (k,X)) holds

( A on L iff A c= L )

for X being non empty set st 0 < k & k + 1 c= card X holds

for A being POINT of (G_ (k,X))

for L being LINE of (G_ (k,X)) holds

( A on L iff A c= L )

proof end;

theorem Th11: :: COMBGRAS:11

for k being Element of NAT

for X being non empty set st 0 < k & k + 1 c= card X holds

G_ (k,X) is Vebleian

for X being non empty set st 0 < k & k + 1 c= card X holds

G_ (k,X) is Vebleian

proof end;

theorem Th12: :: COMBGRAS:12

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) )

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) )

proof end;

theorem :: COMBGRAS:13

for k being Element of NAT

for X being non empty set st 0 < k & k + 1 c= card X holds

G_ (k,X) is Desarguesian

for X being non empty set st 0 < k & k + 1 c= card X holds

G_ (k,X) is Desarguesian

proof end;

:: deftheorem defines clique COMBGRAS:def 2 :

for S being IncProjStr

for K being Subset of the Points of S holds

( K is clique iff for A, B being POINT of S st A in K & B in K holds

ex L being LINE of S st {A,B} on L );

for S being IncProjStr

for K being Subset of the Points of S holds

( K is clique iff for A, B being POINT of S st A in K & B in K holds

ex L being LINE of S st {A,B} on L );

definition

let S be IncProjStr ;

let K be Subset of the Points of S;

end;
let K be Subset of the Points of S;

attr K is maximal_clique means :: COMBGRAS:def 3

( K is clique & ( for U being Subset of the Points of S st U is clique & K c= U holds

U = K ) );

( K is clique & ( for U being Subset of the Points of S st U is clique & K c= U holds

U = K ) );

:: deftheorem defines maximal_clique COMBGRAS:def 3 :

for S being IncProjStr

for K being Subset of the Points of S holds

( K is maximal_clique iff ( K is clique & ( for U being Subset of the Points of S st U is clique & K c= U holds

U = K ) ) );

for S being IncProjStr

for K being Subset of the Points of S holds

( K is maximal_clique iff ( K is clique & ( for U being Subset of the Points of S st U is clique & K c= U holds

U = K ) ) );

definition

let k be Nat;

let X be non empty set ;

let T be Subset of the Points of (G_ (k,X));

end;
let X be non empty set ;

let T be Subset of the Points of (G_ (k,X));

:: deftheorem defines STAR COMBGRAS:def 4 :

for k being Nat

for X being non empty set

for T being Subset of the Points of (G_ (k,X)) holds

( T is STAR iff ex S being Subset of X st

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) );

for k being Nat

for X being non empty set

for T being Subset of the Points of (G_ (k,X)) holds

( T is STAR iff ex S being Subset of X st

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) );

:: deftheorem defines TOP COMBGRAS:def 5 :

for k being Nat

for X being non empty set

for T being Subset of the Points of (G_ (k,X)) holds

( T is TOP iff ex S being Subset of X st

( card S = k + 1 & T = { A where A is Subset of X : ( card A = k & A c= S ) } ) );

for k being Nat

for X being non empty set

for T being Subset of the Points of (G_ (k,X)) holds

( T is TOP iff ex S being Subset of X st

( card S = k + 1 & T = { A where A is Subset of X : ( card A = k & A c= S ) } ) );

theorem Th14: :: COMBGRAS:14

for k being Element of NAT

for X being non empty set st 2 <= k & k + 2 c= card X holds

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

K is maximal_clique

for X being non empty set st 2 <= k & k + 2 c= card X holds

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

K is maximal_clique

proof end;

theorem Th15: :: COMBGRAS:15

for k being Element of NAT

for X being non empty set st 2 <= k & k + 2 c= card X holds

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

( not K is maximal_clique or K is STAR or K is TOP )

for X being non empty set st 2 <= k & k + 2 c= card X holds

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

( not K is maximal_clique or K is STAR or K is TOP )

proof end;

definition

let S1, S2 be IncProjStr ;

attr c_{3} is strict ;

struct IncProjMap over S1,S2 -> ;

aggr IncProjMap(# point-map, line-map #) -> IncProjMap over S1,S2;

sel point-map c_{3} -> Function of the Points of S1, the Points of S2;

sel line-map c_{3} -> Function of the Lines of S1, the Lines of S2;

end;
attr c

struct IncProjMap over S1,S2 -> ;

aggr IncProjMap(# point-map, line-map #) -> IncProjMap over S1,S2;

sel point-map c

sel line-map c

definition

let S1, S2 be IncProjStr ;

let F be IncProjMap over S1,S2;

let a be POINT of S1;

coherence

the point-map of F . a is POINT of S2 ;

end;
let F be IncProjMap over S1,S2;

let a be POINT of S1;

coherence

the point-map of F . a is POINT of S2 ;

:: deftheorem defines . COMBGRAS:def 6 :

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for a being POINT of S1 holds F . a = the point-map of F . a;

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for a being POINT of S1 holds F . a = the point-map of F . a;

definition

let S1, S2 be IncProjStr ;

let F be IncProjMap over S1,S2;

let L be LINE of S1;

coherence

the line-map of F . L is LINE of S2 ;

end;
let F be IncProjMap over S1,S2;

let L be LINE of S1;

coherence

the line-map of F . L is LINE of S2 ;

:: deftheorem defines . COMBGRAS:def 7 :

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for L being LINE of S1 holds F . L = the line-map of F . L;

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for L being LINE of S1 holds F . L = the line-map of F . L;

theorem Th16: :: COMBGRAS:16

for S1, S2 being IncProjStr

for F1, F2 being IncProjMap over S1,S2 st ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( for L being LINE of S1 holds F1 . L = F2 . L ) holds

IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)

for F1, F2 being IncProjMap over S1,S2 st ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( for L being LINE of S1 holds F1 . L = F2 . L ) holds

IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)

proof end;

definition

let S1, S2 be IncProjStr ;

let F be IncProjMap over S1,S2;

end;
let F be IncProjMap over S1,S2;

attr F is incidence_preserving means :: COMBGRAS:def 8

for A1 being POINT of S1

for L1 being LINE of S1 holds

( A1 on L1 iff F . A1 on F . L1 );

for A1 being POINT of S1

for L1 being LINE of S1 holds

( A1 on L1 iff F . A1 on F . L1 );

:: deftheorem defines incidence_preserving COMBGRAS:def 8 :

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2 holds

( F is incidence_preserving iff for A1 being POINT of S1

for L1 being LINE of S1 holds

( A1 on L1 iff F . A1 on F . L1 ) );

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2 holds

( F is incidence_preserving iff for A1 being POINT of S1

for L1 being LINE of S1 holds

( A1 on L1 iff F . A1 on F . L1 ) );

theorem :: COMBGRAS:17

for S1, S2 being IncProjStr

for F1, F2 being IncProjMap over S1,S2 st IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #) & F1 is incidence_preserving holds

F2 is incidence_preserving

for F1, F2 being IncProjMap over S1,S2 st IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #) & F1 is incidence_preserving holds

F2 is incidence_preserving

proof end;

definition

let S be IncProjStr ;

let F be IncProjMap over S,S;

end;
let F be IncProjMap over S,S;

attr F is automorphism means :: COMBGRAS:def 9

( the line-map of F is bijective & the point-map of F is bijective & F is incidence_preserving );

( the line-map of F is bijective & the point-map of F is bijective & F is incidence_preserving );

:: deftheorem defines automorphism COMBGRAS:def 9 :

for S being IncProjStr

for F being IncProjMap over S,S holds

( F is automorphism iff ( the line-map of F is bijective & the point-map of F is bijective & F is incidence_preserving ) );

for S being IncProjStr

for F being IncProjMap over S,S holds

( F is automorphism iff ( the line-map of F is bijective & the point-map of F is bijective & F is incidence_preserving ) );

definition

let S1, S2 be IncProjStr ;

let F be IncProjMap over S1,S2;

let K be Subset of the Points of S1;

coherence

the point-map of F .: K is Subset of the Points of S2

end;
let F be IncProjMap over S1,S2;

let K be Subset of the Points of S1;

coherence

the point-map of F .: K is Subset of the Points of S2

proof end;

:: deftheorem defines .: COMBGRAS:def 10 :

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for K being Subset of the Points of S1 holds F .: K = the point-map of F .: K;

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for K being Subset of the Points of S1 holds F .: K = the point-map of F .: K;

definition

let S1, S2 be IncProjStr ;

let F be IncProjMap over S1,S2;

let K be Subset of the Points of S2;

coherence

the point-map of F " K is Subset of the Points of S1

end;
let F be IncProjMap over S1,S2;

let K be Subset of the Points of S2;

coherence

the point-map of F " K is Subset of the Points of S1

proof end;

:: deftheorem defines " COMBGRAS:def 11 :

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for K being Subset of the Points of S2 holds F " K = the point-map of F " K;

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for K being Subset of the Points of S2 holds F " K = the point-map of F " K;

definition

let X be set ;

let A be finite set ;

{ B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } is Subset of (bool X)

end;
let A be finite set ;

func ^^ (A,X) -> Subset of (bool X) equals :: COMBGRAS:def 12

{ B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } ;

coherence { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } ;

{ B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } is Subset of (bool X)

proof end;

:: deftheorem defines ^^ COMBGRAS:def 12 :

for X being set

for A being finite set holds ^^ (A,X) = { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } ;

for X being set

for A being finite set holds ^^ (A,X) = { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } ;

definition

let k be Nat;

let X be non empty set ;

assume A1: ( 0 < k & k + 1 c= card X ) ;

let A be finite set ;

assume A2: card A = k - 1 ;

coherence

^^ (A,X) is Subset of the Points of (G_ (k,X))

end;
let X be non empty set ;

assume A1: ( 0 < k & k + 1 c= card X ) ;

let A be finite set ;

assume A2: card A = k - 1 ;

coherence

^^ (A,X) is Subset of the Points of (G_ (k,X))

proof end;

:: deftheorem Def13 defines ^^ COMBGRAS:def 13 :

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for A being finite set st card A = k - 1 holds

^^ (A,X,k) = ^^ (A,X);

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for A being finite set st card A = k - 1 holds

^^ (A,X,k) = ^^ (A,X);

theorem Th18: :: COMBGRAS:18

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for K being Subset of the Points of S1 holds F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) }

for F being IncProjMap over S1,S2

for K being Subset of the Points of S1 holds F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) }

proof end;

theorem :: COMBGRAS:19

for S1, S2 being IncProjStr

for F being IncProjMap over S1,S2

for K being Subset of the Points of S2 holds F " K = { A where A is POINT of S1 : ex B being POINT of S2 st

( B in K & F . A = B ) }

for F being IncProjMap over S1,S2

for K being Subset of the Points of S2 holds F " K = { A where A is POINT of S1 : ex B being POINT of S2 st

( B in K & F . A = B ) }

proof end;

theorem Th20: :: COMBGRAS:20

for S being IncProjStr

for F being IncProjMap over S,S

for K being Subset of the Points of S st F is incidence_preserving & K is clique holds

F .: K is clique

for F being IncProjMap over S,S

for K being Subset of the Points of S st F is incidence_preserving & K is clique holds

F .: K is clique

proof end;

theorem Th21: :: COMBGRAS:21

for S being IncProjStr

for F being IncProjMap over S,S

for K being Subset of the Points of S st F is incidence_preserving & the line-map of F is onto & K is clique holds

F " K is clique

for F being IncProjMap over S,S

for K being Subset of the Points of S st F is incidence_preserving & the line-map of F is onto & K is clique holds

F " K is clique

proof end;

theorem Th22: :: COMBGRAS:22

for S being IncProjStr

for F being IncProjMap over S,S

for K being Subset of the Points of S st F is automorphism & K is maximal_clique holds

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

for F being IncProjMap over S,S

for K being Subset of the Points of S st F is automorphism & K is maximal_clique holds

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

proof end;

theorem Th23: :: COMBGRAS:23

for k being 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 )

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 )

proof end;

definition

let k be Nat;

let X be non empty set ;

assume A1: ( 0 < k & k + 1 c= card X ) ;

let s be Permutation of X;

ex b_{1} being strict IncProjMap over G_ (k,X), G_ (k,X) st

( ( for A being POINT of (G_ (k,X)) holds b_{1} . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b_{1} . L = s .: L ) )

for b_{1}, b_{2} being strict IncProjMap over G_ (k,X), G_ (k,X) st ( for A being POINT of (G_ (k,X)) holds b_{1} . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b_{1} . L = s .: L ) & ( for A being POINT of (G_ (k,X)) holds b_{2} . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b_{2} . L = s .: L ) holds

b_{1} = b_{2}

end;
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 over G_ (k,X), G_ (k,X) means :Def14: :: COMBGRAS:def 14

( ( 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 ( ( 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 ) );

ex b

( ( for A being POINT of (G_ (k,X)) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines incprojmap COMBGRAS:def 14 :

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for s being Permutation of X

for b_{4} being strict IncProjMap over G_ (k,X), G_ (k,X) holds

( b_{4} = incprojmap (k,s) iff ( ( for A being POINT of (G_ (k,X)) holds b_{4} . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b_{4} . L = s .: L ) ) );

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for s being Permutation of X

for b

( b

theorem Th24: :: COMBGRAS:24

for k being Nat

for X being non empty set st k = 1 & k + 1 c= card X holds

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

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

for X being non empty set st k = 1 & k + 1 c= card X holds

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

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

proof end;

theorem Th25: :: COMBGRAS:25

for k being Nat

for X being non empty set st 1 < k & card X = k + 1 holds

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

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

for X being non empty set st 1 < k & card X = k + 1 holds

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

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

proof end;

theorem Th26: :: COMBGRAS:26

for k being Element of NAT

for X being non empty set st 0 < k & k + 1 c= card X holds

for T being Subset of the Points of (G_ (k,X))

for S being Subset of X st card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } holds

S = meet T

for X being non empty set st 0 < k & k + 1 c= card X holds

for T being Subset of the Points of (G_ (k,X))

for S being Subset of X st card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } holds

S = meet T

proof end;

theorem :: COMBGRAS:27

for k being Element of NAT

for X being non empty set st 0 < k & k + 1 c= card X holds

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

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

for X being non empty set st 0 < k & k + 1 c= card X holds

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

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

proof end;

theorem Th28: :: COMBGRAS:28

for k being Element of NAT

for X being non empty set st 0 < k & k + 1 c= card X holds

for T1, T2 being Subset of the Points of (G_ (k,X)) st T1 is STAR & T2 is STAR & meet T1 = meet T2 holds

T1 = T2

for X being non empty set st 0 < k & k + 1 c= card X holds

for T1, T2 being Subset of the Points of (G_ (k,X)) st T1 is STAR & T2 is STAR & meet T1 = meet T2 holds

T1 = T2

proof end;

theorem Th29: :: COMBGRAS:29

for k being Element of NAT

for X being non empty set st k + 1 c= card X holds

for A being finite Subset of X st card A = k - 1 holds

^^ (A,X,k) is STAR

for X being non empty set st k + 1 c= card X holds

for A being finite Subset of X st card A = k - 1 holds

^^ (A,X,k) is STAR

proof end;

theorem Th30: :: COMBGRAS:30

for k being Element of NAT

for X being non empty set st k + 1 c= card X holds

for A being finite Subset of X st card A = k - 1 holds

meet (^^ (A,X,k)) = A

for X being non empty set st k + 1 c= card X holds

for A being finite Subset of X st card A = k - 1 holds

meet (^^ (A,X,k)) = A

proof end;

theorem Th31: :: COMBGRAS:31

for k being Nat

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

ex H being IncProjMap over G_ (k,X), G_ (k,X) st

( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))

for B being finite set st B = A holds

H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )

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

ex H being IncProjMap over G_ (k,X), G_ (k,X) st

( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))

for B being finite set st B = A holds

H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )

proof end;

theorem Th32: :: COMBGRAS:32

for k being Nat

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)

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)

proof end;

theorem Th33: :: COMBGRAS:33

for k being 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

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

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

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

proof end;

theorem Th34: :: COMBGRAS:34

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

for s being Permutation of X holds incprojmap (k,s) is automorphism

for X being non empty set st 0 < k & k + 1 c= card X holds

for s being Permutation of X holds incprojmap (k,s) is automorphism

proof end;

theorem :: COMBGRAS:35

for k being Nat

for X being non empty set st 0 < k & k + 1 c= card X holds

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

( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )

for X being non empty set st 0 < k & k + 1 c= card X holds

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

( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )

proof end;