let X be TopSpace; :: thesis: for A, B being Subset of X holds Int (A \/ B) c= (Cl A) \/ (Int B)
let A, B be Subset of X; :: thesis: Int (A \/ B) c= (Cl A) \/ (Int B)
(Int (A `)) /\ (Cl (B `)) c= Cl ((A `) /\ (B `)) by Th3;
then (Cl ((A `) /\ (B `))) ` c= ((Int (A `)) /\ (Cl (B `))) ` by SUBSET_1:12;
then Int (((A `) /\ (B `)) `) c= ((Int (A `)) /\ (Cl (B `))) ` by TDLAT_3:3;
then Int (((A `) `) \/ ((B `) `)) c= ((Int (A `)) /\ (Cl (B `))) ` by XBOOLE_1:54;
then Int (A \/ B) c= ((Int (A `)) `) \/ ((Cl (B `)) `) by XBOOLE_1:54;
then Int (A \/ B) c= (Cl A) \/ ((Cl (B `)) `) by TDLAT_3:1;
hence Int (A \/ B) c= (Cl A) \/ (Int B) by TOPS_1:def 1; :: thesis: verum