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

per cases ( x in SetPrimenumber f or x in {f} ) by A2, XBOOLE_0:def 3;

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

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: verum

end;

suppose x in {f} ; :: thesis: x in SetPrimenumber g

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

end;

end;