let p be Prime; :: thesis: for l being Nat st p |^ l = 3 holds
p = 3
let l be Nat; :: thesis: ( p |^ l = 3 implies p = 3 )
AB: 3 is Prime by XPRIMES1:3;
AA: not 3 is trivial by NAT_2:28;
assume p |^ l = 3 ; :: thesis: p = 3
then p divides 3 by AA, NEWTON03:47;
then ( p = 3 or p = 1 ) by AB, INT_2:def 4;
hence p = 3 by INT_2:def 4; :: thesis: verum