let p be Prime; :: thesis: NatDivisors (p |^ 4) = {1,p,(p |^ 2),(p |^ 3),(p |^ 4)}
set A = NatDivisors (p |^ 4);
set B = {1,p,(p |^ 2),(p |^ 3),(p |^ 4)};
thus NatDivisors (p |^ 4) c= {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} :: according to XBOOLE_0:def 10 :: thesis: {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} c= NatDivisors (p |^ 4)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NatDivisors (p |^ 4) or x in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} )
assume x in NatDivisors (p |^ 4) ; :: thesis: x in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)}
then ex k being Nat st
( x = k & k <> 0 & k divides p |^ 4 ) ;
hence x in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} by Th85; :: thesis: verum

end;

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} or m in NatDivisors (p |^ 4) )
assume A1: m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} ; :: thesis: m in NatDivisors (p |^ 4)
then reconsider m = m as Nat by ENUMSET1:def 3;
m divides p |^ 4 by A1, Th85;
hence m in NatDivisors (p |^ 4) by A1; :: thesis: verum