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 by Def4;
let Q be Subset of TS; :: thesis:
assume that
A3: Q <> {} and
A4: Q is open ; :: thesis:
P ` meets Q by A2, A3, A4, Th80;
then A5: (P ` ) /\ Q <> {} by XBOOLE_0:def 7;
A6: P misses P ` by XBOOLE_1:79;
P /\ ((P ` ) /\ Q) = (P /\ (P ` )) /\ Q by XBOOLE_1:16
.= ({} TS) /\ Q by A6, XBOOLE_0:def 7
.= {} ;
then A7: P misses (P ` ) /\ Q by XBOOLE_0:def 7;
P ` is open by A1;
then (P ` ) /\ Q is open by A4, Th38;
hence ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) by A5, A7, XBOOLE_1:17; :: thesis:

end;

assume A8: 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:

now

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

end;

then P ` is dense by Th80;
hence P is boundary by Def4; :: thesis: