environ
vocabularies HIDDEN, XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, TARSKI, PRE_TOPC, TOPS_2, RCOMP_1, EQREL_1, STRUCT_0, RELAT_2, BORSUK_1, ORDINAL2, CARD_3, CLASSES1, T_0TOPSP, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CLASSES1, RELAT_2, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_2, BORSUK_1, EQREL_1;
definitions TOPS_2, RELAT_2, RELSET_1, PRE_TOPC;
theorems FUNCT_1, FUNCT_2, EQREL_1, RELAT_1, TOPS_2, BORSUK_1, TARSKI, RELSET_1, XBOOLE_0, RELAT_2, PARTFUN1, ORDERS_1, CLASSES1;
schemes FUNCT_2, RELSET_1;
registrations XBOOLE_0, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC, BORSUK_1, EQREL_1, RELSET_1;
constructors HIDDEN, SETFAM_1, RFINSEQ, TOPS_2, BORSUK_1, CLASSES1;
requirements HIDDEN, SUBSET, BOOLE;
equalities STRUCT_0;
expansions TOPS_2, PRE_TOPC;
Lm1:
for T being non empty TopSpace
for x, y being Point of (T_0-reflex T) st x <> y holds
ex V being Subset of (T_0-reflex T) st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
:: Preliminaries
::