begin
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
::