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:55;
then
(Cl A) ` c= Int (Cl ((Cl A) ` ))
by PRE_TOPC:48, TOPS_1:48;
then
( Cl (Int (Cl ((Cl A) ` ))) c= Cl (Cl ((Cl A) ` )) & Cl ((Cl A) ` ) c= Cl (Int (Cl ((Cl A) ` ))) )
by PRE_TOPC:49, TOPS_1:44;
then
Cl (Int (Cl ((Cl A) ` ))) = Cl ((Cl A) ` )
by XBOOLE_0:def 10;
hence
((((((A - ) ` ) - ) ` ) - ) ` ) - = ((A - ) ` ) -
by TOPS_1:def 1; verum