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 A1: A is closed ; :: thesis: Cl A = A
A2: A c= Cl A by Th48;
for x being set st x in Cl A holds
x in A by A1, Th45;
then Cl A c= A by TARSKI:def 3;
hence Cl A = A by A2, XBOOLE_0:def 10; :: thesis: verum

end;

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