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

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