let X be TopSpace; :: thesis: for B, A being Subset of X st A is closed holds
Int (A \/ B) = Int (A \/ (Int B))
let B, A be Subset of X; :: thesis: ( A is closed implies Int (A \/ B) = Int (A \/ (Int B)) )
A \/ (Int B) c= A \/ B by TOPS_1:16, XBOOLE_1:9;
then A1: Int (A \/ (Int B)) c= Int (A \/ B) by TOPS_1:19;
assume A is closed ; :: thesis: Int (A \/ B) = Int (A \/ (Int B))
then Int (Int (A \/ B)) c= Int (A \/ (Int B)) by Th5, TOPS_1:19;
hence Int (A \/ B) = Int (A \/ (Int B)) by A1; :: thesis: verum