let X be TopSpace; :: thesis: for B, A being Subset of X st A is closed holds
Int (A \/ B) c= A \/ (Int B)
let B, A be Subset of X; :: thesis: ( A is closed implies Int (A \/ B) c= A \/ (Int B) )
assume A is closed ; :: thesis: Int (A \/ B) c= A \/ (Int B)
then ( Cl A = A & Int (A \/ B) c= (Cl A) \/ (Int B) ) by Th4, PRE_TOPC:52;
hence Int (A \/ B) c= A \/ (Int B) ; :: thesis: verum