theorem Th23: :: DUALSP01:9

for X being RealLinearSpace holds the carrier of X --> 0 is linear-Functional of X