theorem Th35: :: RLTOPSP1:35

for X being LinearTopSpace
for a being Point of X holds (transl (a,X)) " = transl ((- a),X)