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:12;
assume C is closed ; :: thesis: C = the carrier of X
then C ` = {} X by A1, A2, TOPS_1:50;
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 :: thesis: for G being Subset of X st G c= A & G is open holds
G = {}
let G be Subset of X; :: thesis: ( G c= A & G is open implies G = {} )
assume that
A4: G c= A and
A5: G is open ; :: thesis: G = {}
A ` c= G ` by A4, SUBSET_1:12;
then G ` = the carrier of X by A3, A5;
hence G = {} by Th1; :: thesis: verum
end;
hence A is boundary by TOPS_1:50; :: thesis: verum