let TS be TopSpace; :: thesis: for K being Subset of TS holds Int (Fr (Fr K)) = {}
let K be Subset of TS; :: thesis: Int (Fr (Fr K)) = {}
set x9 = the Element of Int (Fr (Fr K));
assume A1: Int (Fr (Fr K)) <> {} ; :: thesis: contradiction
then reconsider x = the Element of Int (Fr (Fr K)) as Point of TS by TARSKI:def 3;
A2: not TS is empty by A1;
A3: Int (Fr (Fr K)) c= Fr (Fr K) by Th16;
then x in Fr (Fr K) by A1;
then (Fr K) ` meets Int (Fr (Fr K)) by A1, A2, Th28;
then A4: ((Fr K) `) /\ (Int (Fr (Fr K))) <> {} ;
Fr (Fr K) c= Fr K by Th34;
then Int (Fr (Fr K)) c= Fr K by A3;
then A5: ((Fr K) `) /\ (Fr K) <> {} by A4, XBOOLE_1:3, XBOOLE_1:26;
Fr K misses (Fr K) ` by XBOOLE_1:79;
hence contradiction by A5; :: thesis: verum