let X be TopSpace; :: thesis: for A being Subset of X st A is open & A is closed holds
Int (Cl A) = Cl (Int A)
let A be Subset of X; :: thesis: ( A is open & A is closed implies Int (Cl A) = Cl (Int A) )
assume ( A is open & A is closed ) ; :: thesis: Int (Cl A) = Cl (Int A)
then ( Int A = A & Cl A = A ) by PRE_TOPC:52, TOPS_1:55;
hence Int (Cl A) = Cl (Int A) ; :: thesis: verum