theorem Th1: :: GEOMTRAP:1

for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
OASpace V is OAffinSpace