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

proof

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

proof

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

end;

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

end;

hence NatDivisors (p * p) = {1,p,(p * p)} by a1, NEWTON:81; :: thesis: verum