environ
vocabularies HIDDEN, RELAT_1, FUNCT_1, TOPS_1, ARYTM_1, CONNSP_2, EUCLID, PRE_TOPC, ORDINAL2, METRIC_1, TOPMETR, RCOMP_1, PCOMPS_1, TARSKI, XBOOLE_0, NUMBERS, NAT_1, SUBSET_1, XXREAL_0, ARYTM_3, CARD_1, XXREAL_1, REAL_1;
notations HIDDEN, TARSKI, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, METRIC_1, PCOMPS_1, TOPMETR, T_0TOPSP, EUCLID, TOPREAL9, TOPREALB;
definitions TARSKI, T_0TOPSP;
theorems FUNCT_2, TOPMETR, TOPREAL9, EUCLID, JGRAPH_2, GOBOARD6, TOPS_1, METRIC_1, XBOOLE_1, FRECHET, TOPREAL6, RELAT_1, UNIFORM1, CONNSP_2, TOPGRP_1, ORDINAL1, TOPS_3, YELLOW12, TOPGEN_5;
schemes ;
registrations XBOOLE_0, RELAT_1, MEMBERED, XREAL_0, PRE_TOPC, STRUCT_0, EUCLID, TOPREALB, XXREAL_0, METRIC_1, TOPMETR, TOPREAL9, PCOMPS_1, RCOMP_1, TOPGRP_1, VALUED_0, ORDINAL1;
constructors HIDDEN, TOPREAL9, TOPREALB, TOPS_1, T_0TOPSP, FUNCSDOM, PCOMPS_1;
requirements HIDDEN, SUBSET, REAL;
equalities PCOMPS_1, TOPMETR, TOPREALB;
expansions TARSKI, T_0TOPSP;