let T be TopStruct ; :: thesis: for A, B being Subset of T st A c= B holds
Cl A c= Cl B
let A, B be Subset of T; :: thesis: ( A c= B implies Cl A c= Cl B )
assume A1: A c= B ; :: thesis: Cl A c= Cl B

now

let x be set ; :: thesis: ( x in Cl A implies x in Cl B )
assume A2: x in Cl A ; :: thesis: x in Cl B

now

let D1 be Subset of T; :: thesis: ( D1 is closed & B c= D1 implies x in D1 )
assume A3: D1 is closed ; :: thesis: ( B c= D1 implies x in D1 )
assume B c= D1 ; :: thesis: x in D1
then A c= D1 by A1, XBOOLE_1:1;
hence x in D1 by A2, A3, Th45; :: thesis: verum

end;

hence x in Cl B by A2, Th45; :: thesis: verum

end;

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