environ
vocabularies HIDDEN, STRUCT_0, SETFAM_1, TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, RCOMP_1, RELAT_1, FUNCT_1, ORDINAL2, FUNCOP_1, CARD_5, PRE_TOPC;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELSET_1, STRUCT_0;
definitions TARSKI, STRUCT_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1, XBOOLE_0, XBOOLE_1, FUNCT_1, FUNCT_2, RELAT_1, FUNCOP_1;
schemes SUBSET_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, RELSET_1;
constructors HIDDEN, SETFAM_1, PARTFUN1, STRUCT_0, FUNCOP_1, CARD_1, DOMAIN_1, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities STRUCT_0, SUBSET_1;
expansions TARSKI;
Lm1:
for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
:: The topological space
::