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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in primeNumbers (3,10) or x in {5,7,11,13} )
assume A1: x in primeNumbers (3,10) ; :: thesis: x in {5,7,11,13}
then x in seq (3,10) ;
then consider k being Element of NAT such that
A2: x = k and
A3: ( 1 + 3 <= k & k <= 3 + 10 ) ;
not not k = 4 & ... & not k = 13 by A3;
hence x in {5,7,11,13} 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 {5,7,11,13} or x in primeNumbers (3,10) )
assume x in {5,7,11,13} ; :: thesis: x in primeNumbers (3,10)
then A4: ( x = 5 or x = 7 or x = 11 or x = 13 ) by ENUMSET1:def 2;
then A5: x in SetPrimes by NEWTON:def 6, XPRIMES1:5, XPRIMES1:7, XPRIMES1:11, XPRIMES1:13;
x in seq (3,10) by A4;
hence x in primeNumbers (3,10) by A5, XBOOLE_0:def 4; :: thesis: verum