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