let X be RealNormSpace; :: thesis: for A, B being Subset of X holds Cl (A \/ B) = (Cl A) \/ (Cl B)
let A, B be Subset of X; :: thesis: Cl (A \/ B) = (Cl A) \/ (Cl B)
reconsider A1 = A, B1 = B as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
A1: Cl A1 = Cl A by EQCL1;
A2: Cl B1 = Cl B by EQCL1;
Cl (A1 \/ B1) = Cl (A \/ B) by EQCL1;
hence Cl (A \/ B) = (Cl A) \/ (Cl B) by A1, A2, PRE_TOPC:20; :: thesis: verum