let TS be TopSpace; :: thesis: for P being Subset of TS holds
( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds
Q = {} )
let P be Subset of TS; :: thesis: ( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds
Q = {} )

hereby :: thesis: ( ( for Q being Subset of TS st Q c= P & Q is open holds
Q = {} ) implies P is boundary )

assume P is boundary ; :: thesis: for Q being Subset of TS st Q c= P & Q is open holds
not Q <> {}
then A1: P ` is dense ;
let Q be Subset of TS; :: thesis: ( Q c= P & Q is open implies not Q <> {} )
assume that
A2: Q c= P and
A3: Q is open and
A4: Q <> {} ; :: thesis: contradiction
Q meets P ` by A1, A3, A4, Th45;
hence contradiction by A2, SUBSET_1:24; :: thesis: verum

end;

assume A5: for Q being Subset of TS st Q c= P & Q is open holds
Q = {} ; :: thesis: P is boundary
assume not P is boundary ; :: thesis: contradiction
then not P ` is dense ;
then consider C being Subset of TS such that
A6: C <> {} and
A7: C is open and
A8: P ` misses C by Th45;
C c= P by A8, SUBSET_1:24;
hence contradiction by A5, A6, A7; :: thesis: verum