defpred S_{1}[ 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 )
;

end;

suppose
ex i being positive Integer st i in X
; :: thesis: ex b_{1} being positive ExtInt st

( b_{1} in X & ( for i being positive ExtInt st i in X holds

b_{1} <= i ) )

( b

b

then A2:
ex i being Integer st S_{1}[i]
;

A3: for i being Integer st S_{1}[i] holds

0 <= i ;

consider j0 being Integer such that

A4: S_{1}[j0]
and

A5: for i being Integer st S_{1}[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;A3: for i being Integer st S

0 <= i ;

consider j0 being Integer such that

A4: S

A5: for i being Integer st S

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

suppose A7:
for i being positive Integer holds not i in X
; :: thesis: ex b_{1} being positive ExtInt st

( b_{1} in X & ( for i being positive ExtInt st i in X holds

b_{1} <= i ) )

( b

b

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;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