let X be TopSpace; :: thesis: for A being Subset of X holds
( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
let A be Subset of X; :: thesis: ( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
thus ( A is boundary implies for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ) :: thesis: ( ( for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ) implies A is boundary )

proof

assume A1: Int A = {} ; :: according to TOPS_3:def 1 :: thesis: for F being Subset of X st F is closed holds
Int F = Int (F \/ A)
let F be Subset of X; :: thesis: ( F is closed implies Int F = Int (F \/ A) )
assume F is closed ; :: thesis: Int F = Int (F \/ A)
then Int (F \/ A) = Int (F \/ (Int A)) by Th6;
hence Int F = Int (F \/ A) by A1; :: thesis: verum

end;

assume for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ; :: thesis: A is boundary
then Int ({} X) = Int (({} X) \/ A) ;
hence A is boundary ; :: thesis: verum