let T be TopStruct ; :: thesis: for A being Subset of T holds A c= Cl A
let A be Subset of T; :: thesis: A c= Cl A

now

let x be set ; :: thesis: ( x in A implies x in Cl A )
assume A1: x in A ; :: thesis: x in Cl A
assume not x in Cl A ; :: thesis: contradiction
then ex C being Subset of T st
( C is closed & A c= C & not x in C ) by A1, Th45;
hence contradiction by A1; :: thesis: verum

end;

hence A c= Cl A by TARSKI:def 3; :: thesis: verum