environ
vocabularies HIDDEN, STRUCT_0, SUBSET_1, PRE_TOPC, XBOOLE_0, RCOMP_1, TARSKI, TOPS_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
definitions TARSKI, XBOOLE_0;
theorems PRE_TOPC, TARSKI, SUBSET_1, XBOOLE_0, XBOOLE_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
constructors HIDDEN, SETFAM_1, PRE_TOPC;
requirements HIDDEN, BOOLE, SUBSET;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0;
Lm1:
for TS being TopSpace
for K, L being Subset of TS holds Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
Lm2:
for GX being TopStruct
for T being Subset of GX holds Fr T = (Cl T) \ (Int T)
Lm3:
for TS being TopSpace
for K being Subset of TS holds Cl (Fr K) = Fr K
Lm4:
for TS being TopSpace
for K being Subset of TS holds Int (Fr (Fr K)) = {}
Lm5:
for X, Y, Z being set st X c= Z & Y = Z \ X holds
X c= Z \ Y
:: INTERIOR OF A SET
::