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

proof

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

end;

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