set A = { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square } ;
thus { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square } c= {3} :: according to XBOOLE_0:def 10 :: thesis: {3} c= { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square } or x in {3} )
assume x in { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square } ; :: thesis: x in {3}
then ex p being Prime st
( x = p & (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square ) ;
then x = 3 by Th86;
hence x in {3} by TARSKI:def 1; :: thesis: verum

end;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in {3} or p in { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square } )
assume p in {3} ; :: thesis: p in { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square }
then A1: p = 3 by TARSKI:def 1;
then reconsider p = p as Prime by XPRIMES1:3;
(((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square by A1, Th86;
hence p in { p where p is Prime : (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square } ; :: thesis: verum