defpred S1[ Integer] means ( \$1 in X & \$1 is positive );
per cases ( ex i being positive Integer st i in X or for i being positive Integer holds not i in X ) ;
suppose ex i being positive Integer st i in X ; :: thesis: ex b1 being positive ExtInt st
( b1 in X & ( for i being positive ExtInt st i in X holds
b1 <= i ) )

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

thus j in X by A4; :: thesis: for i being positive ExtInt st i in X holds
j <= i

let i be positive ExtInt; :: thesis: ( i in X implies j <= i )
assume A6: i in X ; :: thesis: j <= i
end;
suppose A7: for i being positive Integer holds not i in X ; :: thesis: ex b1 being positive ExtInt st
( b1 in X & ( for i being positive ExtInt st i in X holds
b1 <= i ) )

take i0 ; :: thesis: ( i0 in X & ( for i being positive ExtInt st i in X holds
i0 <= i ) )

thus i0 in X by A1; :: thesis: for i being positive ExtInt st i in X holds
i0 <= i

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