let T be TopStruct ; :: thesis: for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
let A be Subset of T; :: thesis: ( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
thus ( A is closed implies Cl A = A ) :: thesis: ( T is TopSpace-like & Cl A = A implies A is closed )

proof

assume A is closed ; :: thesis: Cl A = A
then for x being object st x in Cl A holds
x in A by Th15;
then A1: Cl A c= A ;
A c= Cl A by Th18;
hence Cl A = A by A1, XBOOLE_0:def 10; :: thesis: verum

end;

assume A2: T is TopSpace-like ; :: thesis: ( not Cl A = A or A is closed )
then consider F being Subset-Family of T such that
A3: for C being Subset of T holds
( C in F iff ( C is closed & A c= C ) ) and
A4: Cl A = meet F by Th16;
assume A5: Cl A = A ; :: thesis: A is closed
for C being Subset of T st C in F holds
C is closed by A3;
hence A is closed by A2, A5, A4, Th14; :: thesis: verum