let X be TopSpace; :: thesis: for A being Subset of X holds
( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
let A be Subset of X; :: thesis: ( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
thus ( A is boundary implies for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ) :: thesis: ( ( for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ) implies A is boundary )

proof

assume A1: A is boundary ; :: thesis: for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X
let C be Subset of X; :: thesis: ( A ` c= C & C is closed implies C = the carrier of X )
assume A ` c= C ; :: thesis: ( not C is closed or C = the carrier of X )
then A2: C ` c= (A ` ) ` by SUBSET_1:31;
assume C is closed ; :: thesis: C = the carrier of X
then C ` is open ;
then C ` = {} X by A1, A2, TOPS_1:86;
hence C = the carrier of X by Th2; :: thesis: verum

end;

assume A3: for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ; :: thesis: A is boundary

now

let G be Subset of X; :: thesis: ( G c= A & G is open implies G = {} )
assume ( G c= A & G is open ) ; :: thesis: G = {}
then ( A ` c= G ` & G ` is closed ) by SUBSET_1:31;
then G ` = the carrier of X by A3;
hence G = {} by Th1; :: thesis: verum

end;

hence A is boundary by TOPS_1:86; :: thesis: verum