theorem Th17: :: DUALSP01:10

for X being RealLinearSpace holds LinearFunctionals X is linearly-closed