let a be Real; :: thesis: for k being Integer st a >= 0 holds

a #Z k >= 0

let k be Integer; :: thesis: ( a >= 0 implies a #Z k >= 0 )

assume A1: a >= 0 ; :: thesis: a #Z k >= 0

a #Z k >= 0

let k be Integer; :: thesis: ( a >= 0 implies a #Z k >= 0 )

assume A1: a >= 0 ; :: thesis: a #Z k >= 0