let n be Nat; :: thesis: SetPrimenumber n = { k where k is Element of NAT : ( k < n & k is prime ) }
thus SetPrimenumber n c= { k where k is Element of NAT : ( k < n & k is prime ) } :: according to XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : ( k < n & k is prime ) } c= SetPrimenumber n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SetPrimenumber n or x in { k where k is Element of NAT : ( k < n & k is prime ) } )
assume A1: x in SetPrimenumber n ; :: thesis: x in { k where k is Element of NAT : ( k < n & k is prime ) }
then reconsider x = x as Element of NAT ;
A2: x is prime by A1, Def7;
x < n by A1, Def7;
hence x in { k where k is Element of NAT : ( k < n & k is prime ) } by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( k < n & k is prime ) } or x in SetPrimenumber n )
assume x in { k where k is Element of NAT : ( k < n & k is prime ) } ; :: thesis: x in SetPrimenumber n
then ex k being Element of NAT st
( x = k & k < n & k is prime ) ;
hence x in SetPrimenumber n by Def7; :: thesis: verum