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))))
A2: Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18;
A3: Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
then Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19;
then A c= Cl (Int (Cl A)) by A1;
then A \/ (Int (Cl A)) c= (Cl (Int (Cl A))) \/ (Cl (Int (Cl A))) by A2, XBOOLE_1:13;
then A4: A \/ (Int (Cl A)) c= Cl ((Int A) \/ (Int (Cl A))) by A3, XBOOLE_1:12;
(Int A) \/ (Int (Int (Cl A))) c= Int (A \/ (Int (Cl A))) by TOPS_1:20;
then Cl ((Int A) \/ (Int (Cl A))) c= Cl (Int (A \/ (Int (Cl A)))) by PRE_TOPC:19;
hence A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) by A4; :: thesis: verum