defpred S₁[ 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 b₁ being positive ExtInt st
( b₁ in X & ( for i being positive ExtInt st i in X holds
b₁ <= i ) )

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

per cases ( i is Integer or not i is Integer ) ;

suppose i is Integer ; :: thesis: j <= i

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

end;

suppose i is not Integer ; :: thesis: j <= i

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

end;

end;

end;

suppose A7: for i being positive Integer holds not i in X ; :: thesis: ex b₁ being positive ExtInt st
( b₁ in X & ( for i being positive ExtInt st i in X holds
b₁ <= 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;