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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in Cl B )
assume A2: x in Cl A ; :: thesis: x in Cl B
now :: thesis: for D1 being Subset of T st D1 is closed & B c= D1 holds
x in D1
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;
hence x in D1 by A2, A3, Th15; :: thesis: verum
end;
hence x in Cl B by A2, Th15; :: thesis: verum