environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, TOPS_1, TARSKI, RCOMP_1, RELAT_1, CONNSP_1, RELAT_2, SETFAM_1, CONNSP_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1;
definitions TARSKI, COMPTS_1;
theorems TARSKI, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, CONNSP_1, XBOOLE_0, XBOOLE_1, SUBSET_1;
schemes SUBSET_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, TOPS_1, CONNSP_1, COMPTS_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, COMPTS_1;
Lm1:
for X being non empty TopSpace
for X1 being SubSpace of X
for A being Subset of X
for A1 being Subset of X1 st A = A1 holds
(Int A) /\ ([#] X1) c= Int A1
:: A NEIGHBORHOOD OF A POINT
::