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