environ
vocabularies HIDDEN, NUMBERS, CLASSES2, RELAT_1, ZFMISC_1, ORDERS_2, NECKLACE, CARD_1, ARYTM_3, SUBSET_1, XBOOLE_0, TARSKI, XXREAL_0, ORDINAL1, FINSET_1, CLASSES1, STRUCT_0, FUNCT_1, SETFAM_1, NAT_1, CARD_3, NECKLA_2;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELSET_1, PARTIT_2, FINSET_1, CARD_1, ORDINAL1, NUMBERS, CLASSES2, SETFAM_1, CLASSES1, CARD_3, XCMPLX_0, XXREAL_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, ORDERS_2, NECKLACE;
definitions TARSKI;
theorems FUNCT_1, FUNCT_2, ENUMSET1, RELSET_1, ZFMISC_1, XBOOLE_1, TARSKI, ORDINAL1, PARTFUN1, NECKLACE, CLASSES2, CLASSES1, XBOOLE_0, SETFAM_1, CARD_5, NAT_1, STRUCT_0, RELAT_1, CARD_2, XREAL_1, XXREAL_0, XTUPLE_0;
schemes TARSKI, XBOOLE_0, NAT_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XREAL_0, CLASSES2, STRUCT_0, ORDERS_2, CARD_1, CLASSES1, NAT_1;
constructors HIDDEN, NAT_1, CLASSES2, REALSET2, COH_SP, NECKLACE, RELSET_1, PARTIT_2;
requirements HIDDEN, BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
equalities TARSKI;
expansions TARSKI;
theorem Th2:
the
InternalRel of
(Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
definition
existence
ex b1 being Subset of fin_RelStr st
( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
b1 c= M ) )
uniqueness
for b1, b2 being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
b1 c= M ) & ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b2 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b2 & H2 in b2 holds
( union_of (H1,H2) in b2 & sum_of (H1,H2) in b2 ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
b2 c= M ) holds
b1 = b2
end;
Lm1:
the carrier of (Necklace 4) = {0,1,2,3}
by NECKLACE:1, NECKLACE:20;