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:32
.= (T /\ ((Cl T) ` )) \/ (T /\ (Int T)) by XBOOLE_1:23 ;
A2: Int T = T /\ (Int T) by Th44, XBOOLE_1:28;
T c= Cl T by PRE_TOPC:48;
then T misses (Cl T) ` by SUBSET_1:44;
then T \ (Fr T) = {} \/ (Int T) by A1, A2, XBOOLE_0:def 7;
hence Int T = T \ (Fr T) ; :: thesis: verum