let i be Integer; :: thesis: for x being object st x in multiples i holds
x is Multiple of i
let x be object ; :: thesis: ( x in multiples i implies x is Multiple of i )
assume x in multiples i ; :: thesis: x is Multiple of i
then ex m being Multiple of i st x = m ;
hence x is Multiple of i ; :: thesis: verum