theorem Th39: :: WALLIS01:1

for n being Nat
for x being Real st 0 < x & x < PI / 2 holds
( 0 < sin . x & sin . x < 1 )