theorem :: RLTOPSP1:43

for X being LinearTopSpace
for F being Subset-Family of X st F is finite & F = { P where P is bounded Subset of X : verum } holds
union F is bounded