environ
vocabularies HIDDEN, FUNCT_1, XBOOLE_0, RELAT_1, FUNCT_4, SUBSET_1, NUMBERS, ABIAN, FUNCT_7, ARYTM_3, COHSP_1, TARSKI, FUNCOP_1, ZFMISC_1, SETFAM_1, FUNCT_2, LATTICES, STRUCT_0, ORDINAL1, ORDINAL2, EQREL_1, CARD_1, BINOP_1, LATTICE3, PBOOLE, FILTER_0, FILTER_1, WELLORD1, RELAT_2, ORDERS_1, ORDERS_2, XXREAL_0, REWRITE1, XXREAL_2, SEQM_3, KNASTER, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, RELAT_2, ORDERS_1, STRUCT_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, SETFAM_1, FUNCT_4, WELLORD1, ORDINAL2, COHSP_1, LATTICES, LATTICE3, QUANTAL1, ORDERS_2, ABIAN;
definitions TARSKI, FUNCT_1, COHSP_1, LATTICE3, QUANTAL1, XBOOLE_0, ABIAN;
theorems TARSKI, SETFAM_1, ZFMISC_1, RELAT_1, FUNCT_1, FUNCOP_1, FUNCT_2, FUNCT_4, CARD_1, COHSP_1, LATTICES, LATTICE3, QUANTAL1, FILTER_0, FILTER_1, BOOLEALG, WELLORD1, RELSET_1, ORDERS_2, RELAT_2, ORDINAL1, CARD_3, XBOOLE_0, XBOOLE_1, FUNCT_7, PARTFUN1, ORDERS_1, NAT_1, XTUPLE_0;
schemes NAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, ORDINAL2;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, CARD_1, STRUCT_0, LATTICES, LATTICE3, QUANTAL1, XCMPLX_0, NAT_1;
constructors HIDDEN, WELLORD1, WELLORD2, BINOP_1, DOMAIN_1, ORDINAL2, NAT_1, ABIAN, BOOLEALG, QUANTAL1, COHSP_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities RELAT_1, LATTICE3, WELLORD1, ORDINAL1, CARD_1;
expansions TARSKI, RELAT_1, FUNCT_1, COHSP_1, LATTICE3, QUANTAL1, XBOOLE_0, ABIAN;
scheme
Knaster{
F1()
-> set ,
F2(
object )
-> set } :
ex
D being
set st
(
F2(
D)
= D &
D c= F1() )
provided
A1:
for
X,
Y being
set st
X c= Y holds
F2(
X)
c= F2(
Y)
and A2:
F2(
F1())
c= F1()
Lm1:
for O1, O2 being Ordinal holds
( O1 c< O2 or O1 = O2 or O2 c< O1 )