let TS be TopSpace; :: thesis:
let P be Subset of TS; :: thesis:
assume A1: P is closed ; :: thesis:

hereby :: thesis:

assume P is boundary ; :: thesis:
then A2: P ` is dense ;
A3: P misses P ` by XBOOLE_1:79;
let Q be Subset of TS; :: thesis:
assume that
A4: Q <> {} and
A5: Q is open ; :: thesis:
P /\ ((P `) /\ Q) = (P /\ (P `)) /\ Q by XBOOLE_1:16
.= ({} TS) /\ Q by A3
.= {} ;
then A6: P misses (P `) /\ Q ;
P ` meets Q by A2, A4, A5, Th45;
then (P `) /\ Q <> {} ;
hence ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) by A1, A5, A6, XBOOLE_1:17; :: thesis:

end;

assume A7: for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) ; :: thesis:

let Q be Subset of TS; :: thesis:
assume that
A8: Q <> {} and
A9: Q is open ; :: thesis:
consider G being Subset of TS such that
A10: G c= Q and
A11: G <> {} and
G is open and
A12: P misses G by A7, A8, A9;
G misses (P `) ` by A12;
then G c= P ` by SUBSET_1:24;
hence P ` meets Q by A10, A11, XBOOLE_1:67; :: thesis:

end;

then P ` is dense by Th45;
hence P is boundary ; :: thesis: