thus primeNumbers (0,10) c= {2,3,5,7} :: according to XBOOLE_0:def 10 :: thesis: {2,3,5,7} c= primeNumbers (0,10)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in primeNumbers (0,10) or x in {2,3,5,7} )
assume A1: x in primeNumbers (0,10) ; :: thesis: x in {2,3,5,7}
then x in seq (0,10) ;
then consider k being Element of NAT such that
A2: x = k and
A3: ( 1 + 0 <= k & k <= 0 + 10 ) ;
A4: k is prime by A1, A2, NEWTON:def 6;
not not k = 1 & ... & not k = 10 by A3;
hence x in {2,3,5,7} by A2, A4, ENUMSET1:def 2, XPRIMES0:4, XPRIMES0:6, XPRIMES0:8, XPRIMES0:9, XPRIMES0:10; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {2,3,5,7} or x in primeNumbers (0,10) )
assume x in {2,3,5,7} ; :: thesis: x in primeNumbers (0,10)
then A5: ( x = 2 or x = 3 or x = 5 or x = 7 ) by ENUMSET1:def 2;
then A6: x in SetPrimes by NEWTON:def 6, XPRIMES1:2, XPRIMES1:3, XPRIMES1:5, XPRIMES1:7;
x in seq (0,10) by A5;
hence x in primeNumbers (0,10) by A6, XBOOLE_0:def 4; :: thesis: verum