theorem Th15: :: BASEL_1:15

for r being Real holds
( tan r = (cot r) " & cot r = (tan r) " )