environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, RELAT_1, ZFMISC_1, SETFAM_1, TARSKI, PARTFUN1, RELAT_2, XBOOLE_0, FINSEQ_1, XXREAL_0, FUNCT_1, ARYTM_3, ORDINAL4, ARYTM_1, NAT_1, CARD_1, EQREL_1, MCART_1, CARD_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, DOMAIN_1, SUBSET_1, XCMPLX_0, XXREAL_0, RELAT_1, RELAT_2, SETFAM_1, FINSEQ_1, FUNCT_1, ORDINAL1, NUMBERS, NAT_1, FUNCT_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1;
definitions TARSKI, RELAT_1, RELAT_2, XBOOLE_0, PARTFUN1, SETFAM_1;
theorems RELAT_1, RELAT_2, RELSET_1, SETFAM_1, ZFMISC_1, TARSKI, FINSEQ_1, NAT_1, XBOOLE_0, XBOOLE_1, ORDERS_1, PARTFUN1, XREAL_1, XXREAL_0, FUNCT_1, FUNCT_3, FUNCT_2, MCART_1, SUBSET_1, SETWISEO, XTUPLE_0;
schemes SUBSET_1, RELSET_1, FINSEQ_1, NAT_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, PARTFUN1, XXREAL_0, XREAL_0, FINSEQ_1, RELAT_1, ORDINAL1, RELSET_1, FUNCT_2, ZFMISC_1, FUNCT_1, RELAT_2;
constructors HIDDEN, SETFAM_1, RELAT_2, PARTFUN1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, RELSET_1, FUNCT_3, BINOP_1, DOMAIN_1, XTUPLE_0, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TARSKI, RELAT_1, SUBSET_1, BINOP_1;
expansions TARSKI, RELAT_1, RELAT_2, XBOOLE_0;
Lm1:
for X being set
for x, y being object
for R being Relation of X st [x,y] in R holds
( x in X & y in X )
scheme
ExEqRel{
F1()
-> set ,
P1[
object ,
object ] } :
provided
A1:
for
x being
object st
x in F1() holds
P1[
x,
x]
and A2:
for
x,
y being
object st
P1[
x,
y] holds
P1[
y,
x]
and A3:
for
x,
y,
z being
object st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
Lm2:
for X being set
for y being object
for EqR being Equivalence_Relation of X
for x being object st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
Lm3:
for X being non empty set
for x being Element of X
for F being Part-Family of X
for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )