environ
Vocabularies HIDDEN, NUMBERS, ZFMISC_1, RELAT_2, REWRITE1, XBOOLE_0, ORDERS_2, PRELAMB, SUBSET_1, IDEAL_1, TARSKI, RELAT_1, STRUCT_0, ARYTM_3, XXREAL_0, WAYBEL_0, LATTICE3, LATTICES, EQREL_1, CARD_FIL, YELLOW_0, ORDINAL2, BINOP_1, FUNCT_1, OPOSET_1, CARD_1, FUNCOP_1, FINSUB_1, YELLOW_1, ARYTM_0, WELLORD2, FINSEQ_1, FUNCT_7, NAT_1, ORDINAL4, FINSET_1, FINSEQ_5, ARYTM_1, ABCMIZ_0, ABIAN;
Notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, SUBSET_1, ORDINAL1, FINSUB_1, CARD_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FINSET_1, FINSEQ_1, FUNCT_4, ALG_1, FINSEQ_5, NUMBERS, XCMPLX_0, NAT_1, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, REWRITE1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, XXREAL_0;
Definitions TARSKI, XBOOLE_0, RELAT_2, FUNCT_1, FINSEQ_1, LATTICE3, REWRITE1, YELLOW_0, WAYBEL_0, RELSET_1;
Theorems TARSKI, XBOOLE_0, XBOOLE_1, SUBSET_1, FINSUB_1, NAT_1, FINSEQ_1, CARD_1, TREES_1, FINSEQ_5, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_4, YELLOW_7, WAYBEL_6, WAYBEL_8, ZFMISC_1, FINSEQ_2, FINSEQ_3, HILBERT2, REWRITE1, ORDINAL1, XREAL_1, XXREAL_0, PRE_POLY;
Schemes XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, RECDEF_1, RELSET_1, ORDERS_1;
Registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_2, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, REWRITE1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, YELLOW_9, ORDINAL1, CARD_1, RELSET_1;
Constructors HIDDEN, FINSUB_1, NAT_1, FINSEQ_5, REWRITE1, BORSUK_1, LATTICE3, WAYBEL_0, YELLOW_1, FUNCOP_1, XREAL_0;
Requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin
begin
begin
begin
scheme
MinimalFiniteSet{
P1[
set ] } :
ex
A being
finite set st
(
P1[
A] & ( for
B being
set st
B c= A &
P1[
B] holds
B = A ) )
provided
begin
scheme
RedInd{
F1()
-> non
empty set ,
P1[
set ,
set ],
F2()
-> Relation of
F1() } :
provided
A1:
for
x,
y being
Element of
F1() st
[x,y] in F2() holds
P1[
x,
y]
and A2:
for
x being
Element of
F1() holds
P1[
x,
x]
and A3:
for
x,
y,
z being
Element of
F1() st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
begin