environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_2, FINSEQ_1, RELAT_1, FINSUB_1, FINSET_1, SETFAM_1, TARSKI, RELAT_2, WAYBEL_4, ORDERS_2, STRUCT_0, XXREAL_0, NAT_1, CARD_1, PRE_POLY, FUNCT_1, MARGREL1, XBOOLEAN, PARTFUN1, BINARI_3, EUCLID, ARYTM_3, POWER, ORDINAL4, PBOOLE, CARD_3, ZFMISC_1, MCART_1, EQREL_1, FUNCOP_1, BINARITH, FUNCT_4, ARMSTRNG, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, FINSET_1, FINSUB_1, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, PARTFUN1, CARD_1, ORDINAL1, NUMBERS, FUNCT_4, FUNCT_1, ORDERS_2, MCART_1, EQREL_1, CARD_3, PBOOLE, XCMPLX_0, STRUCT_0, WAYBEL_4, FINSEQ_1, FUNCOP_1, MARGREL1, FINSEQ_2, BINARITH, BINARI_3, SERIES_1, EUCLID, XXREAL_0, NAT_1, PRE_POLY, FUNCT_2;
definitions TARSKI, RELAT_2, YELLOW_0, WAYBEL_4, FINSUB_1, PRE_POLY;
theorems TARSKI, RELSET_1, ZFMISC_1, EQREL_1, MCART_1, RELAT_1, RELAT_2, XBOOLE_0, XBOOLE_1, ORDERS_2, ENUMSET1, FINSET_1, SUBSET_1, SETFAM_1, MSSUBFAM, TREES_1, FUNCT_1, FINSEQ_4, FINSEQ_1, FINSEQ_2, FUNCOP_1, CARD_3, BINARI_3, NAT_1, EUCLID, FUNCT_2, BINARITH, POWER, FUNCT_4, PARTFUN1, NUMBERS, XREAL_1, ORDERS_1, XXREAL_0, ORDINAL1, PRE_POLY, CARD_1, XTUPLE_0, BAGORDER;
schemes FINSET_1, NAT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, XBOOLE_0, CLASSES1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, EQREL_1, MARGREL1, FINSEQ_2, CARD_3, ORDERS_2, PRE_POLY, CARD_1, RELSET_1, STRUCT_0, FUNCT_4, XTUPLE_0;
constructors HIDDEN, SETFAM_1, XXREAL_0, FINSEQOP, SERIES_1, BINARITH, EUCLID, MATRLIN, WAYBEL_4, BINARI_3, RELSET_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
equalities FINSEQ_2, SUBSET_1, XBOOLEAN;
expansions TARSKI, RELAT_2, WAYBEL_4, FINSUB_1;
scheme
SubsetSEq{
F1()
-> set ,
P1[
set ] } :
for
X1,
X2 being
Subset of
F1() st ( for
y being
set holds
(
y in X1 iff
P1[
y] ) ) & ( for
y being
set holds
(
y in X2 iff
P1[
y] ) ) holds
X1 = X2
theorem
for
X being
set for
A,
B,
A9,
B9 being
Subset of
X holds
(
[A,B] >= [A9,B9] iff (
A c= A9 &
B9 c= B ) ) ;
Lm3:
for X, F, BB being set st F = { [a,b] where a, b is Subset of X : for c being set st c in BB & a c= c holds
b c= c } holds
for x, y being Subset of X holds
( [x,y] in F iff for c being set st c in BB & x c= c holds
y c= c )
:: they are the irreducible elements \ X