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 Th16;
assume P is open ; :: thesis: Fr P is nowhere_dense
then A2: Int P = P by Th23;
then P misses Fr P by Th39;
then A3: P /\ (Fr P) = {} TS ;
Int (P /\ (Fr P)) = P /\ (Int (Fr P)) by A2, Th17;
then P /\ (Int (Fr P)) = {} by A3;
then A4: P misses Int (Fr P) ;
Int (Fr P) c= Int (Cl P) by Th19, XBOOLE_1:17;
then A5: Int (Fr P) c= Cl P by A1;
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, Th48;
then the Element of Int (Fr P) in Cl P by A5;
hence contradiction by A4, A8, A7, Th12; :: thesis: verum
end;
hence Fr P is nowhere_dense ; :: thesis: verum