environ
vocabularies HIDDEN, SETFAM_1, XBOOLE_0, CANTOR_1, TARSKI, PRE_TOPC, RLVECT_3, RELAT_1, PRALG_1, FUNCT_1, PBOOLE, FUNCOP_1, WAYBEL_3, STRUCT_0, SUBSET_1, CARD_3, RLVECT_2, RCOMP_1, FUNCT_4, MONOID_0, ORDINAL2, FUNCTOR0, PARTFUN1, FUNCT_6, BORSUK_1, FUNCT_3, GROUP_6, WAYBEL_1, FUNCT_2, T_0TOPSP, TOPS_2, CARD_1, ZFMISC_1, RELAT_2, ORDERS_2, WAYBEL11, YELLOW_9, YELLOW_1, LATTICE3, FILTER_1, XXREAL_0, WAYBEL_0, CARD_FIL, FINSET_1, REWRITE1, WAYBEL_8, LATTICES, CAT_1, WAYBEL_9, WAYBEL18;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, RELAT_1, PBOOLE, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, ORDINAL1, NUMBERS, STRUCT_0, PRE_TOPC, T_0TOPSP, FUNCT_3, FUNCT_6, FUNCT_7, CARD_3, FUNCOP_1, MONOID_0, PRALG_1, ORDERS_2, LATTICE3, YELLOW_1, CANTOR_1, FINSET_1, TOPS_2, BORSUK_1, TMAP_1, YELLOW_0, YELLOW_9, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11;
definitions TARSKI, PRE_TOPC, FUNCOP_1, WAYBEL_1, WAYBEL_3, XBOOLE_0, PRALG_1;
theorems TARSKI, PRE_TOPC, ENUMSET1, ZFMISC_1, T_0TOPSP, TOPS_1, TOPS_2, FINSET_1, FUNCT_2, FUNCT_3, RELAT_1, FUNCT_1, BORSUK_1, FUNCOP_1, CANTOR_1, LATTICE3, ORDERS_2, MSSUBFAM, PRALG_1, CARD_3, WAYBEL_3, FUNCT_6, FUNCT_7, TMAP_1, YELLOW_9, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_7, WAYBEL_8, WAYBEL11, WAYBEL13, WAYBEL14, RELSET_1, SETFAM_1, XBOOLE_0, XBOOLE_1, ORDERS_1, MONOID_0, CARD_1, PARTFUN1;
schemes SUBSET_1, CLASSES1, FUNCT_1, FRAENKEL;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, STRUCT_0, PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, WAYBEL_3, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL17, RELAT_1, CARD_1;
constructors HIDDEN, FUNCT_3, FUNCT_7, TOPS_2, BORSUK_1, LATTICE3, TMAP_1, T_0TOPSP, CANTOR_1, MONOID_0, PRALG_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL11, YELLOW_9, BINOP_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities STRUCT_0, ORDINAL1;
expansions TARSKI, PRE_TOPC, WAYBEL_1, XBOOLE_0;
definition
existence
ex b1 being strict TopStruct st
( the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} )
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} & the carrier of b2 = {0,1} & the topology of b2 = {{},{1},{0,1}} holds
b1 = b2
;
end;
Lm1:
Sierpinski_Space is T_0