take
REAL --> t
; :: thesis: ( REAL --> t is t -periodic & REAL --> t is real-valued )

thus ( REAL --> t is t -periodic & REAL --> t is real-valued ) ; :: thesis: verum

thus ( REAL --> t is t -periodic & REAL --> t is real-valued ) ; :: thesis: verum