take <*> the carrier of F_Rat ; :: thesis: <*> the carrier of F_Rat is INT -valued
thus <*> the carrier of F_Rat is INT -valued ; :: thesis: verum