let f be Prime; :: thesis:
let g be Nat; :: thesis:
assume A1: f < g ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in (SetPrimenumber f) \/ {f} ; :: thesis:
then reconsider x = x as Nat ;

per cases by A2, XBOOLE_0:def 3;

suppose A3: x in SetPrimenumber f ; :: thesis:

then x < f by Def7;
then A4: x < g by A1, XXREAL_0:2;
x is prime by A3, Def7;
hence x in SetPrimenumber g by A4, Def7; :: thesis:

end;

suppose x in {f} ; :: thesis:

then x = f by TARSKI:def 1;
hence x in SetPrimenumber g by A1, Def7; :: thesis:

end;

end;