let TS be TopSpace; :: thesis: for P being Subset of TS st P is open holds
Fr P is nowhere_dense
let P be Subset of TS; :: thesis: ( P is open implies Fr P is nowhere_dense )
A1: Int (Cl P) c= Cl P by Th44;
assume P is open ; :: thesis: Fr P is nowhere_dense
then A2: Int P = P by Th55;
then P misses Fr P by Th73;
then A3: P /\ (Fr P) = {} TS by XBOOLE_0:def 7;
Int (P /\ (Fr P)) = P /\ (Int (Fr P)) by A2, Th46;
then P /\ (Int (Fr P)) = {} by A3;
then A4: P misses Int (Fr P) by XBOOLE_0:def 7;
Int (Fr P) c= Int (Cl P) by Th48, XBOOLE_1:17;
then A5: Int (Fr P) c= Cl P by A1, XBOOLE_1:1;
Fr P is boundary

proof

set x = the Element of Int (Fr P);
assume A6: not Fr P is boundary ; :: thesis: contradiction
then A7: not TS is empty ;
A8: Int (Fr P) <> {} by A6, Th84;
then the Element of Int (Fr P) in Cl P by A5, TARSKI:def 3;
hence contradiction by A4, A8, A7, Th39; :: thesis: verum

end;

hence Fr P is nowhere_dense ; :: thesis: verum