environ
vocabularies HIDDEN, STRUCT_0, SUBSET_1, PRE_TOPC, FUNCT_1, FUNCT_2, RELAT_1, VALUED_1, XBOOLE_0, ALGSTR_0, TARSKI, GROUP_1, ZFMISC_1, ORDINAL2, TOPS_2, CONNSP_2, TOPS_1, RCOMP_1, T_0TOPSP, BINOP_1, UNIALG_1, CARD_5, SETFAM_1, COMPTS_1, RLVECT_3, TOPGRP_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, CARD_1, TOPS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, SETFAM_1, GROUP_2, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, GROUP_1, CONNSP_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP, CANTOR_1, YELLOW_8;
definitions TARSKI, FUNCT_1, PRE_TOPC, GROUP_1, STRUCT_0, TOPS_1, TOPS_2, CONNSP_2, FUNCT_2, T_0TOPSP, XBOOLE_0;
theorems PRE_TOPC, RELAT_1, TOPS_1, TOPS_2, BINOP_1, FUNCT_2, GROUP_1, GROUP_2, TARSKI, FUNCT_1, BORSUK_1, TEX_2, ZFMISC_1, CONNSP_2, URYSOHN1, T_0TOPSP, YELLOW_8, YELLOW_9, XBOOLE_0, XBOOLE_1, STRUCT_0, RELSET_1;
schemes BINOP_1, FUNCT_2, XBOOLE_0;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_1, GROUP_1, COMPTS_1, BORSUK_1, TEX_1, BORSUK_2, RELSET_1, CARD_1, ALGSTR_0;
constructors HIDDEN, TOPS_1, TOPS_2, COMPTS_1, GROUP_2, BORSUK_1, GRCAT_1, URYSOHN1, T_0TOPSP, CANTOR_1, YELLOW_8, TEX_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities STRUCT_0, XBOOLE_0, BINOP_1, SUBSET_1, COMPTS_1, RELAT_1, ALGSTR_0, GROUP_2;
expansions TARSKI, FUNCT_1, PRE_TOPC, TOPS_2, FUNCT_2, T_0TOPSP, RELAT_1;
Lm1:
for G being Group
for A, B being Subset of G st A c= B holds
A " c= B "
Lm2:
for T being TopStruct
for f being Function of T,T st T is empty holds
f is being_homeomorphism