let T be TopSpace; :: thesis: for A, B being Subset of T holds (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B)))
let A, B be Subset of T; :: thesis: (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B)))
set C = Int A;
set D = Int B;
(Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl ((Int A) /\ (Int B))) by TDLAT_1:7;
hence (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B))) by TOPS_1:17; :: thesis: verum