:: 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₄ being strict IncProjMap over G_ (k,X), G_ (k,X) holds
( b₄ = incprojmap (k,s) iff ( ( for A being POINT of (G_ (k,X)) holds b₄ . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b₄ . L = s .: L ) ) );