theorem Th22b: :: DUALSP01:14

for X being RealLinearSpace holds 0. (X *') = the carrier of X --> 0