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:24;
thus Cl (X \/ Y) = Cl (A \/ B) by TOPREAL6:80
.= (Cl A) \/ (Cl B) by PRE_TOPC:50
.= (Cl X) \/ (Cl B) by TOPREAL6:80
.= (Cl X) \/ (Cl Y) by TOPREAL6:80 ; :: thesis: verum