let i, j be Integer; :: thesis: ( j in multiples i iff i divides j )
thus ( j in multiples i implies i divides j ) :: thesis: ( i divides j implies j in multiples i )

proof

assume j in multiples i ; :: thesis: i divides j
then j is Multiple of i by Th61;
hence i divides j by Def15; :: thesis: verum

end;

assume i divides j ; :: thesis: j in multiples i
then j is Multiple of i by Def15;
hence j in multiples i ; :: thesis: verum