take <*1*> ; :: thesis: <*1*> is nonnegative
thus <*1*> is nonnegative ; :: thesis: verum