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 by PRE_TOPC:22;
hence Int (A \/ B) c= A \/ (Int B) by Th4; :: thesis: verum