theorem :: RLTOPSP1:42

for X being LinearTopSpace
for P being bounded Subset of X
for Q being Subset of X st Q c= P holds
Q is bounded