let X be LinearTopSpace; :: thesis: for V being closed Subset of X
for r being non zero Real holds r * V is closed
let V be closed Subset of X; :: thesis: for r being non zero Real holds r * V is closed
let r be non zero Real; :: thesis: r * V is closed
(mlt (r,X)) .: V = r * V by Th47;
hence r * V is closed by TOPS_2:72; :: thesis: verum