environ
vocabularies HIDDEN, NUMBERS, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, RELAT_2, STRUCT_0, FINSET_1, ORDERS_2, CARD_1, CAT_1, YELLOW_0, WELLORD1, NECKLA_2, NECKLACE, SUBSET_1, FUNCT_1, XXREAL_0, SEQM_3, REWRITE1, FINSEQ_1, NAT_1, ARYTM_3, FINSEQ_5, EQREL_1, MSUALG_5, CLASSES2, FUNCOP_1, FUNCT_4, ARYTM_1, NECKLA_3, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, DOMAIN_1, STRUCT_0, ORDERS_2, WAYBEL_1, FUNCOP_1, CLASSES2, NECKLACE, WAYBEL_0, FUNCT_4, REWRITE1, FINSEQ_1, FINSEQ_5, EQREL_1, MSUALG_5, YELLOW_0, NECKLA_2, WELLORD1;
definitions XBOOLE_0, TARSKI, NECKLACE, RELAT_2;
theorems RELSET_1, NECKLACE, XBOOLE_0, WAYBEL_0, YELLOW_0, FUNCT_1, FUNCT_2, ORDERS_2, RELAT_2, SUBSET_1, ZFMISC_1, XBOOLE_1, TARSKI, MCART_1, CLASSES2, CLASSES1, NECKLA_2, FUNCOP_1, ENUMSET1, RELAT_1, SYSREL, PARTFUN1, GROUP_6, CARD_2, REWRITE1, FINSEQ_1, FINSEQ_3, FINSEQ_5, NAT_1, EQREL_1, MSUALG_6, MSUALG_5, CARD_1, NAT_2, FUNCT_4, FUNCT_3, WAYBEL_1, YELLOW_6, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, STRUCT_0, XTUPLE_0;
schemes NAT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, FINSEQ_1, STRUCT_0, ORDERS_2, YELLOW_0, NECKLACE, NECKLA_2, ORDINAL1, FUNCT_4, RELSET_1, ZFMISC_1;
constructors HIDDEN, NAT_1, EQREL_1, CLASSES1, TOLER_1, CLASSES2, FINSEQ_5, REWRITE1, REALSET2, MSUALG_5, ORDERS_3, WAYBEL_1, NECKLACE, NECKLA_2, RELSET_1, FUNCT_4;
requirements HIDDEN, BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
equalities TARSKI, FUNCOP_1, WELLORD1, STRUCT_0, ORDINAL1, CARD_1;
expansions XBOOLE_0, TARSKI, NECKLACE, RELAT_2;
theorem
for
a,
b,
c,
d being
set holds
id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]}
theorem Th3:
for
a,
b,
c,
d,
e,
f,
g,
h being
set holds
[:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}
theorem Th11:
the
InternalRel of
(ComplRelStr (Necklace 4)) = {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}
Lm1:
for X being non empty finite set
for A, B being non empty set st X = A \/ B & A misses B holds
card A in Segm (card X)
theorem Th38:
for
G being non
empty symmetric irreflexive RelStr for
a,
b,
c,
d being
Element of
G for
Z being
Subset of
G st
Z = {a,b,c,d} &
a,
b,
c,
d are_mutually_distinct &
[a,b] in the
InternalRel of
G &
[b,c] in the
InternalRel of
G &
[c,d] in the
InternalRel of
G & not
[a,c] in the
InternalRel of
G & not
[a,d] in the
InternalRel of
G & not
[b,d] in the
InternalRel of
G holds
subrelstr Z embeds Necklace 4