let TS be TopSpace; :: thesis: for P being Subset of TS st P is closed holds
( P is boundary iff 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 ) )
let P be Subset of TS; :: thesis: ( P is closed implies ( P is boundary iff 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 ) ) )
assume A1: P is closed ; :: thesis: ( P is boundary iff 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 ) )

hereby :: thesis: ( ( 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 ) ) implies P is boundary )

assume P is boundary ; :: thesis: 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 )
then A2: P ` is dense ;
A3: P misses P ` by XBOOLE_1:79;
let Q be Subset of TS; :: thesis: ( Q <> {} & Q is open implies ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) )
assume that
A4: Q <> {} and
A5: Q is open ; :: thesis: ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G )
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: verum

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: P is boundary

now :: thesis: for Q being Subset of TS st Q <> {} & Q is open holds
P ` meets Q

let Q be Subset of TS; :: thesis: ( Q <> {} & Q is open implies P ` meets Q )
assume that
A8: Q <> {} and
A9: Q is open ; :: thesis: P ` meets Q
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: verum

end;

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