defpred S₁[ Integer] means ( $1 in X & $1 is positive );

suppose ex i being positive Integer st i in X ; :: thesis:

then A2: ex i being Integer st S₁[i] ;
A3: for i being Integer st S₁[i] holds
0 <= i ;
consider j0 being Integer such that
A4: S₁[j0] and
A5: for i being Integer st S₁[i] holds
j0 <= i from INT_1:sch 5(A3, A2);
reconsider j = j0 as positive ExtInt by A4;
take j ; :: thesis:
thus j in X by A4; :: thesis:
let i be positive ExtInt; :: thesis:
assume A6: i in X ; :: thesis:

suppose i is Integer ; :: thesis:

then reconsider i1 = i as Integer ;
j0 <= i1 by A6, A5;
hence j <= i ; :: thesis:

end;

suppose i is not Integer ; :: thesis:

then i = +infty by Def1;
hence j <= i by XXREAL_0:3; :: thesis:

end;

end;

end;

suppose A7: for i being positive Integer holds not i in X ; :: thesis:

take i0 ; :: thesis:
thus i0 in X by A1; :: thesis:
let i be positive ExtInt; :: thesis:
assume i in X ; :: thesis:
then ( i is not positive Integer & +infty <= +infty ) by A7;
then i = +infty by Def1;
hence i0 <= i by XXREAL_0:3; :: thesis:

end;

end;