let T be TopSpace; :: thesis: for A being Subset of T st Int (Cl A) c= A holds
Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))
let A be Subset of T; :: thesis: ( Int (Cl A) c= A implies Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) )
assume A1: Int (Cl A) c= A ; :: thesis: Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))
A2: Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16;
A3: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
then Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19;
then Int (Cl (Int A)) c= A by A1;
then (Int (Cl (Int A))) /\ (Int (Cl (Int A))) c= A /\ (Cl (Int A)) by A2, XBOOLE_1:27;
then A4: Int ((Cl A) /\ (Cl (Int A))) c= A /\ (Cl (Int A)) by A3, XBOOLE_1:28;
Cl (A /\ (Cl (Int A))) c= (Cl A) /\ (Cl (Cl (Int A))) by PRE_TOPC:21;
then Int (Cl (A /\ (Cl (Int A)))) c= Int ((Cl A) /\ (Cl (Int A))) by TOPS_1:19;
hence Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) by A4; :: thesis: verum