environ
vocabularies HIDDEN, RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_2, FUNCT_1, SUBSET_1, FINSET_1, NUMBERS, NAT_1, INT_1, ARYTM_3, CARD_1, XXREAL_0, ARYTM_1, INT_2, CARD_2, FINSEQ_1, ORDINAL4, FINSEQ_2, XCMPLX_0, NEWTON, RFINSEQ, FRIENDS1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, ENUMSET1, FUNCT_1, ORDINAL1, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, CARD_1, CARD_2, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, INT_2, FINSEQ_1, FINSEQ_2, NEWTON, RFINSEQ, NAT_D;
definitions XBOOLE_0, TARSKI, RELAT_1, FUNCT_1;
theorems TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, INT_2, INT_1, SIMPLEX1, CARD_2, CARD_1, FINSET_1, XBOOLE_1, FUNCT_1, FUNCT_2, WELLORD2, FINSEQ_6, NAT_D, INT_4, NAT_3, INT_5, NAT_1, XREAL_1, XXREAL_0, NEWTON, FINSEQ_5, FINSEQ_3, RFINSEQ, FINSEQ_1, FINSEQ_2, SUBSET_1, XTUPLE_0;
schemes CLASSES1, RELAT_1, NAT_1, FUNCT_2;
registrations RELAT_1, FINSEQ_2, XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, NEWTON;
constructors HIDDEN, RELAT_2, DOMAIN_1, RELSET_1, NAT_1, REAL_1, CARD_2, WELLORD2, FINSEQ_2, NEWTON, RFINSEQ, NAT_D;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
equalities CARD_2, RELAT_1, FINSEQ_1, CARD_1, ORDINAL1;
expansions XBOOLE_0;
Lm1:
for k, n being Nat holds
( n * k = n *` k & n + k = n +` k )
Lm2:
for x being object
for R being Relation st R is irreflexive holds
not [x,x] in R
Lm3:
for x, y being object
for R being Relation st R is symmetric & [x,y] in R holds
[y,x] in R
Lm4:
for k being Nat
for p being FinSequence st not k in dom p holds
(p /^ k) ^ (p | k) = p
Lm5:
for x, y, z being object
for P being finite Relation
for t being object st P is friendship_graph_like & x <> y & [x,z] in P & [z,y] in P & [x,t] in P & [t,y] in P holds
z = t