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 that
A1: A is open and
A2: A is closed ; :: thesis: Int (Cl A) = Cl (Int A)
A3: Cl A = A by A2, PRE_TOPC:22;
Int A = A by A1, TOPS_1:23;
hence Int (Cl A) = Cl (Int A) by A3; :: thesis: verum