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:31;
then Int (((A ` ) /\ (B ` )) ` ) c= ((Int (A ` )) /\ (Cl (B ` ))) ` by TDLAT_3:4;
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:2;
hence Int (A \/ B) c= (Cl A) \/ (Int B) by TOPS_1:def 1; :: thesis: verum