take 1_. F_Real ; :: thesis: ( 1_. F_Real is monic & 1_. F_Real is INT -valued )
thus ( 1_. F_Real is monic & 1_. F_Real is INT -valued ) ; :: thesis: verum