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:20
.= Cl ((Cl A) \/ ((Cl A) `)) by PRE_TOPC:20
.= Cl ([#] T) by PRE_TOPC:2
.= [#] T by TOPS_1:2 ; :: thesis: verum