let T be TopSpace; :: thesis: for A being Subset of T st A c= Cl (Int A) holds
A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))
let A be Subset of T; :: thesis: ( A c= Cl (Int A) implies A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) )
assume A1: A c= Cl (Int A) ; :: thesis: A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))
( Int (Cl A) = Int (Int (Cl A)) & (Int A) \/ (Int (Int (Cl A))) c= Int (A \/ (Int (Cl A))) ) by TOPS_1:49;
then A2: Cl ((Int A) \/ (Int (Cl A))) c= Cl (Int (A \/ (Int (Cl A)))) by PRE_TOPC:49;
A3: Int A c= Int (Cl A) by PRE_TOPC:48, TOPS_1:48;
then Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:49;
then ( Int (Cl A) c= Cl (Int (Cl A)) & A c= Cl (Int (Cl A)) ) by A1, PRE_TOPC:48, XBOOLE_1:1;
then A \/ (Int (Cl A)) c= (Cl (Int (Cl A))) \/ (Cl (Int (Cl A))) by XBOOLE_1:13;
then A \/ (Int (Cl A)) c= Cl ((Int A) \/ (Int (Cl A))) by A3, XBOOLE_1:12;
hence A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) by A2, XBOOLE_1:1; :: thesis: verum