let p1, p2 be Prime; :: thesis: ( p1 divides p2 implies p1 = p2 )
assume p1 divides p2 ; :: thesis: p1 = p2
then ( p1 = 1 or p1 = p2 ) by INT_2:def 4;
hence p1 = p2 by INT_2:def 4; :: thesis: verum