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

proof

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

end;

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