environ
vocabularies HIDDEN, SETFAM_1, SUBSET_1, TARSKI, PRE_TOPC, RCOMP_1, RLVECT_3, FINSET_1, XBOOLE_0, FINSUB_1, SETWISEO, ZFMISC_1, STRUCT_0, FUNCT_1, RELAT_1, CARD_3, NUMBERS, FUNCOP_1, CARD_1, NAT_1, CANTOR_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSUB_1, SETWISEO, PROB_1, STRUCT_0, PRE_TOPC, TOPS_2, CARD_3, FUNCOP_1;
definitions PRE_TOPC, TARSKI, XBOOLE_0;
theorems ZFMISC_1, PRE_TOPC, SUBSET_1, SETFAM_1, FINSET_1, FUNCT_2, FUNCT_1, TARSKI, FINSUB_1, RELAT_1, XBOOLE_0, XBOOLE_1, TOPS_2, EQREL_1;
schemes SUBSET_1, FUNCT_2, SETWISEO;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCOP_1, FINSET_1, CARD_3, PRE_TOPC, FUNCT_1, TOPS_2;
constructors HIDDEN, SETFAM_1, FUNCOP_1, SETWISEO, CARD_3, TOPS_2, RELSET_1, PROB_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities STRUCT_0;
expansions TARSKI, XBOOLE_0;
definition
existence
ex b1 being non empty strict TopSpace st
( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) )
uniqueness
for b1, b2 being non empty strict TopSpace st the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) & the carrier of b2 = product (NAT --> {0,1}) & ex P being prebasis of b2 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) holds
b1 = b2
end;