take sin ; :: thesis: sin is periodic
thus sin is periodic by Lm2; :: thesis: verum