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

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