take sin ; :: thesis: ( sin is periodic & sin is real-valued )
thus ( sin is periodic & sin is real-valued ) by L1, Def2; :: thesis: verum