let T be non empty TopSpace; for A being Subset of T holds ((((((A -) `) -) `) -) `) - = ((A -) `) -
let A be Subset of T; ((((((A -) `) -) `) -) `) - = ((A -) `) -
set B = Cl ((Cl A) `);
set U = (Cl A) ` ;
(Cl A) ` = Int ((Cl A) `)
by TOPS_1:23;
then
(Cl A) ` c= Int (Cl ((Cl A) `))
by PRE_TOPC:18, TOPS_1:19;
then
( Cl (Int (Cl ((Cl A) `))) c= Cl (Cl ((Cl A) `)) & Cl ((Cl A) `) c= Cl (Int (Cl ((Cl A) `))) )
by PRE_TOPC:19, TOPS_1:16;
then
Cl (Int (Cl ((Cl A) `))) = Cl ((Cl A) `)
by XBOOLE_0:def 10;
hence
((((((A -) `) -) `) -) `) - = ((A -) `) -
by TOPS_1:def 1; verum