take 1. ; :: thesis: ( 1. is real & 1. is ext-integer & 1. is positive )
thus ( 1. is real & 1. is ext-integer & 1. is positive ) ; :: thesis: verum