assume PrimeDivisors 1 <> {} ; :: thesis: contradiction
then consider p being object such that
A1: p in { k where k is Prime : k divides 1 } by XBOOLE_0:def 1;
consider pp being Prime such that
A2: ( pp = p & pp divides 1 ) by A1;
( pp = 1 or pp = - 1 ) by A2, INT_2:13;
hence contradiction by INT_2:def 4; :: thesis: verum