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