let T be TopSpace; :: thesis: for A being Subset of T holds Cl (A \/ (Int (A ` ))) = [#] T
let A be Subset of T; :: thesis: Cl (A \/ (Int (A ` ))) = [#] T
thus Cl (A \/ (Int (A ` ))) = Cl (A \/ ((Cl ((A ` ) ` )) ` )) by TOPS_1:def 1
.= (Cl (Cl A)) \/ (Cl ((Cl A) ` )) by PRE_TOPC:50
.= Cl ((Cl A) \/ ((Cl A) ` )) by PRE_TOPC:50
.= Cl ([#] T) by PRE_TOPC:18
.= [#] T by TOPS_1:27 ; :: thesis: verum