environ
vocabularies HIDDEN, FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1, ORDINAL1, FUNCT_1, RELAT_1, CARD_FIL, LATTICES, PBOOLE, STRUCT_0, ORDERS_2, XXREAL_0, LATTICE3, WAYBEL_0, YELLOW_1, NUMBERS, FINSEQ_1, NAT_1, YELLOW13, ARYTM_3, PRE_TOPC, RCOMP_1, CANTOR_1, FILTER_0, DICKSON, RELAT_2, MEMBERED, XXREAL_1, FUNCT_3, FINSUB_1, WAYBEL_7, YELLOW19, COMPTS_1, CARD_3, CARDFIL2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, SETFAM_1, FINSET_1, ORDINAL1, CARD_1, RELSET_1, CARD_FIL, DOMAIN_1, NAT_1, STRUCT_0, LATTICES, FILTER_0, NUMBERS, LATTICE3, YELLOW_0, ORDERS_2, YELLOW_1, XXREAL_0, FINSEQ_1, CANTOR_1, NAT_LAT, DICKSON, WAYBEL_0, MEMBERED, FUNCT_3, FUNCT_2, FINSUB_1, PBOOLE, ZFMISC_1, PRE_TOPC, WAYBEL_7, COMPTS_1, YELLOW19, YELLOW_6, MCART_1, CARD_3;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ORDINAL1, SETFAM_1, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, CARD_FIL, FILTER_0, LATTICE3, WAYBEL_0, YELLOW_1, WAYBEL_7, WAYBEL_8, WAYBEL15, WAYBEL16, AFINSQ_1, NAT_1, FINSEQ_1, PRE_TOPC, CONNSP_2, CANTOR_1, DICKSON, XTUPLE_0, AFINSQ_2, SUBSET_1, PRE_CIRC, PARTFUN1, YELLOW19, CARD_3;
schemes FUNCT_2, NAT_1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, CARD_1, STRUCT_0, LATTICE3, WAYBEL_0, YELLOW_1, WAYBEL_7, RELAT_1, XREAL_0, NAT_1, DICKSON, MEMBERED, FUNCT_2, CANTOR_1, PBOOLE, PROB_1, SETFAM_1, YELLOW19, WAYBEL_3, CARD_3;
constructors HIDDEN, CARD_FIL, WAYBEL_7, CANTOR_1, NAT_LAT, DICKSON, FINSUB_1, PROB_1, NAT_1, COMPTS_1, YELLOW19, BORSUK_1, ORDERS_3, WAYBEL11, XXREAL_2, SIMPLEX0;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL;
equalities STRUCT_0, LATTICE3, YELLOW_1, CARD_FIL, DICKSON, WAYBEL_0;
expansions TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDERS_2, WAYBEL_0, FINSUB_1;
Lm01:
for X being non empty set
for SFX being non empty with_non-empty_elements cap-closed upper Subset-Family of X holds SFX is Filter of X
Lm02:
for X being non empty set
for FX being Filter of X holds FX is non empty with_non-empty_elements cap-closed upper Subset-Family of X
Lm3:
for p being Element of OrderedNAT
for p0 being Element of NAT st p = p0 holds
{ x where x is Element of NAT : p0 <= x } = { x where x is Element of OrderedNAT : p <= x }
Lm4:
for p being Element of OrderedNAT holds { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } = { x where x is Element of OrderedNAT : p <= x }