let X be TopSpace; :: thesis: for A being Subset of X holds
( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
let A be Subset of X; :: thesis: ( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
thus ( A is boundary implies for G being Subset of X st G <> {} & G is open holds
A ` meets G ) :: thesis: ( ( for G being Subset of X st G <> {} & G is open holds
A ` meets G ) implies A is boundary )

proof

assume A1: A is boundary ; :: thesis: for G being Subset of X st G <> {} & G is open holds
A ` meets G
let G be Subset of X; :: thesis: ( G <> {} & G is open implies A ` meets G )
assume A2: G <> {} ; :: thesis: ( not G is open or A ` meets G )
assume A3: G is open ; :: thesis: A ` meets G
assume A ` misses G ; :: thesis: contradiction
then G c= A by SUBSET_1:44;
hence contradiction by A1, A2, A3, TOPS_1:86; :: thesis: verum

end;

assume A4: for G being Subset of X st G <> {} & G is open holds
A ` meets G ; :: thesis: A is boundary
assume A5: Int A <> {} ; :: according to TOPS_3:def 1 :: thesis: contradiction
( Int A is open & Int A c= A ) by TOPS_1:44;
then ( A ` meets Int A & Int A misses A ` & (A ` ) /\ (Int A) = (Int A) /\ (A ` ) ) by A4, A5, SUBSET_1:44;
hence contradiction ; :: thesis: verum