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 :: thesis: for x being object st x in A holds
x in Cl A

let x be object ; :: 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, Th15;
hence contradiction by A1; :: thesis: verum

end;

hence A c= Cl A ; :: thesis: verum