let X, Y be Subset of REAL; :: thesis: Cl (X \/ Y) = (Cl X) \/ (Cl Y)
reconsider A = X, B = Y as Subset of R^1 by TOPMETR:17;
thus Cl (X \/ Y) = Cl (A \/ B) by JORDAN5A:24
.= (Cl A) \/ (Cl B) by PRE_TOPC:20
.= (Cl X) \/ (Cl B) by JORDAN5A:24
.= (Cl X) \/ (Cl Y) by JORDAN5A:24 ; :: thesis: verum