environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, RLVECT_1, RUSUB_4, SUBSET_1, ARYTM_3, SUPINF_2, TARSKI, ALGSTR_0, ARYTM_1, REAL_1, RELAT_1, BHSP_1, RLSUB_1, STRUCT_0, RVSUM_1, PROB_2, CARD_1, NORMSP_1, SQUARE_1, XXREAL_0, RLVECT_3, PCOMPS_1, SETFAM_1, PRE_TOPC, METRIC_1, RCOMP_1, COMPLEX1, RUSUB_5;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, PRE_TOPC, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1, SQUARE_1, BHSP_1, BHSP_2, RUSUB_1, RUSUB_3, RUSUB_4;
definitions XBOOLE_0, TARSKI, PRE_TOPC;
theorems RLVECT_1, TARSKI, XBOOLE_0, XBOOLE_1, RUSUB_1, SUBSET_1, RLSUB_1, PRE_TOPC, RUSUB_4, BHSP_1, BHSP_2, SQUARE_1, ZFMISC_1, SETFAM_1, ABSVALUE, TOPS_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, STRUCT_0;
schemes DOMAIN_1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, XXREAL_0, XREAL_0, STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RUSUB_4, SQUARE_1, ORDINAL1;
constructors HIDDEN, SETFAM_1, REAL_1, SQUARE_1, MEMBERED, COMPLEX1, REALSET1, PRE_TOPC, RLVECT_3, BHSP_2, RUSUB_3, RUSUB_4, XXREAL_0;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RLVECT_1, SQUARE_1, SUBSET_1, STRUCT_0;
expansions XBOOLE_0, TARSKI, PRE_TOPC, STRUCT_0;