environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, CARD_FIL, YELLOW_1, LATTICES, PRE_TOPC, CONNSP_2, STRUCT_0, TARSKI, ZFMISC_1, WAYBEL_0, XXREAL_0, TOPS_1, WAYBEL_7, RCOMP_1, RELAT_1, RELAT_2, FUNCT_1, FINSET_1, SETFAM_1, LATTICE3, ORDERS_2, WELLORD2, ORDINAL1, MCART_1, YELLOW_6, SEQ_2, METRIC_1, CANTOR_1, ARYTM_0, ARYTM_3, CLASSES1, INT_2, YELLOW_0, CAT_1, BHSP_3, YELLOW19;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, MCART_1, SETFAM_1, FINSET_1, FUNCT_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, CLASSES1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, YELLOW_6, WAYBEL_9, YELLOW_7, WAYBEL32;
definitions TARSKI, TOPS_2, WAYBEL_0, WAYBEL_7, WAYBEL_9, XBOOLE_0, FINSET_1;
theorems TARSKI, SETFAM_1, FUNCT_2, FINSET_1, FUNCT_1, CLASSES1, RELAT_1, ZFMISC_1, RELAT_2, SUBSET_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, WAYBEL_8, WAYBEL_9, YELLOW_5, YELLOW_6, YELLOW_7, WAYBEL12, WAYBEL21, WAYBEL32, XBOOLE_0, XBOOLE_1;
schemes RELSET_1, FUNCT_2, FUNCT_1;
registrations SUBSET_1, RELAT_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_6, WAYBEL_7, WAYBEL_9, WAYBEL32, RELSET_1, XTUPLE_0;
constructors HIDDEN, CLASSES1, TOLER_1, TOPS_1, TOPS_2, CONNSP_2, CANTOR_1, WAYBEL_1, WAYBEL_7, WAYBEL32, COMPTS_1, RELSET_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, BOOLE, SUBSET;
equalities SUBSET_1, WAYBEL_0, XBOOLE_0, STRUCT_0;
expansions TARSKI, SUBSET_1, TOPS_2, WAYBEL_0, WAYBEL_7, WAYBEL_9, XBOOLE_0, FINSET_1;
definition
let L be non
empty 1-sorted ;
let O be non
empty Subset of
L;
let F be
Filter of
(BoolePoset O);
existence
ex b1 being non empty strict NetStr over L st
( the carrier of b1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) )
uniqueness
for b1, b2 being non empty strict NetStr over L st the carrier of b1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) & the carrier of b2 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b2 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b2 holds b2 . i = i `1 ) holds
b1 = b2
end;
Lm1:
for T being non empty TopSpace st T is compact holds
for N being net of T ex x being Point of T st x is_a_cluster_point_of N
Lm2:
for T being non empty TopSpace st ( for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ) holds
T is compact