take ArProg (1,1) ; :: thesis: ArProg (1,1) is integer-valued
thus ArProg (1,1) is integer-valued ; :: thesis: verum