let p be Prime; :: thesis: NatDivisors p = {1,p}
a1: NatDivisors (p |^ 1) = { (p |^ k) where k is Element of NAT : k <= 1 } by NAT_5:19;
{ (p |^ k) where k is Element of NAT : k <= 1 } = {1,p}

proof

thus { (p |^ k) where k is Element of NAT : k <= 1 } c= {1,p} :: according to XBOOLE_0:def 10 :: thesis: {1,p} c= { (p |^ k) where k is Element of NAT : k <= 1 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (p |^ k) where k is Element of NAT : k <= 1 } or x in {1,p} )
assume x in { (p |^ k) where k is Element of NAT : k <= 1 } ; :: thesis: x in {1,p}
then consider kk being Element of NAT such that
A2: ( x = p |^ kk & kk <= 1 ) ;
not not kk = 0 & ... & not kk = 1 by A2;
then ( x = 1 or x = p |^ 1 ) by NEWTON:4, A2;
hence x in {1,p} by TARSKI:def 2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1,p} or x in { (p |^ k) where k is Element of NAT : k <= 1 } )
assume x in {1,p} ; :: thesis: x in { (p |^ k) where k is Element of NAT : k <= 1 }
then ( x = 1 or x = p ) by TARSKI:def 2;
then ( x = p |^ 0 or x = p |^ 1 ) by NEWTON:4;
hence x in { (p |^ k) where k is Element of NAT : k <= 1 } ; :: thesis: verum

end;

hence NatDivisors p = {1,p} by a1; :: thesis: verum