environ
vocabularies HIDDEN, NUMBERS, INCSP_1, SUBSET_1, CARD_1, XBOOLE_0, ARYTM_3, TARSKI, ORDINAL1, FINSET_1, RELAT_1, ARYTM_1, NAT_1, FUNCT_1, XXREAL_0, FDIFF_1, WELLORD2, ZFMISC_1, ANPROJ_2, AFF_2, MOD_4, FUNCT_2, PRE_POLY, SETFAM_1, COMBGRAS;
notations HIDDEN, TARSKI, XBOOLE_0, CARD_1, SUBSET_1, ORDINAL1, ENUMSET1, ZFMISC_1, SETFAM_1, DOMAIN_1, FINSET_1, RELAT_1, RELSET_1, WELLORD2, NUMBERS, INCSP_1, XXREAL_0, XCMPLX_0, REAL_1, FUNCT_1, FUNCT_2, INCPROJ, NAT_1;
definitions TARSKI, INCSP_1, INCPROJ, FUNCT_1;
theorems ENUMSET1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, XREAL_1, SETFAM_1, PENCIL_1, INCSP_1, WELLORD2, CARD_1, CARD_2, NAT_1, ORDINAL1, CARD_FIL, STIRL2_1, XXREAL_0, FUNCT_1, FUNCT_2, RELAT_1, RELSET_1;
schemes FUNCT_1, NAT_1, CLASSES1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, XREAL_0, NAT_1, CARD_1, INCSP_1, RELSET_1;
constructors HIDDEN, SETFAM_1, WELLORD2, DOMAIN_1, REAL_1, NAT_1, BINOP_2, INCPROJ, RELSET_1, XREAL_0, INT_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities RELAT_1, ORDINAL1, CARD_1;
expansions TARSKI, INCSP_1, INCPROJ, FUNCT_1;
theorem Th5:
for
X,
Y,
Z being
set st
X \ Y = X \ Z &
Y c= X &
Z c= X holds
Y = Z
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) )
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;
existence
ex b1 being strict IncProjMap over 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 over 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;
theorem Th32:
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)