theorem Th13: :: SIN_COS9:13

for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
tan . x = tan x