let GX be TopStruct ; :: thesis: for T being Subset of GX holds Int T = T \ (Fr T)
let T be Subset of GX; :: thesis: Int T = T \ (Fr T)
((Cl (T `)) `) \/ ((Cl T) `) = ((Cl T) /\ (Cl (T `))) ` by XBOOLE_1:54;
then A1: T \ (Fr T) = T /\ (((Cl (T `)) `) \/ ((Cl T) `)) by SUBSET_1:13
.= (T /\ ((Cl T) `)) \/ (T /\ (Int T)) by XBOOLE_1:23 ;
T c= Cl T by PRE_TOPC:18;
then A2: T misses (Cl T) ` by SUBSET_1:24;
Int T = T /\ (Int T) by Th16, XBOOLE_1:28;
then T \ (Fr T) = {} \/ (Int T) by A1, A2;
hence Int T = T \ (Fr T) ; :: thesis: verum