let TS be TopSpace; :: thesis: for P being Subset of TS st P is condensed holds
Int (Fr P) = {}
let P be Subset of TS; :: thesis: ( P is condensed implies Int (Fr P) = {} )
set x = the Element of Int (Fr P);
assume A1: P is condensed ; :: thesis: Int (Fr P) = {}
then P c= Cl (Int P) ;
then A2: (Cl (Int P)) ` c= P ` by SUBSET_1:12;
assume A3: Int (Fr P) <> {} ; :: thesis: contradiction
then reconsider x99 = the Element of Int (Fr P) as Point of TS by TARSKI:def 3;
A4: Int (Fr P) = (Cl (((Cl P) `) \/ ((Cl (P `)) `))) ` by XBOOLE_1:54
.= ((Cl ((Cl P) `)) \/ (Cl ((Cl (P `)) `))) ` by PRE_TOPC:20
.= (Int (Cl P)) /\ ((Cl (Int P)) `) by XBOOLE_1:53 ;
then A5: x99 in Int (Cl P) by A3, XBOOLE_0:def 4;
A6: x99 in (Cl (Int P)) ` by A4, A3, XBOOLE_0:def 4;
Int (Cl P) c= P by A1;
hence contradiction by A2, A5, A6, XBOOLE_0:def 5; :: thesis: verum