suppose A1: X = {} ; :: thesis:

take 0 ; :: thesis:
thus ( ( X <> {} implies ex i being Nat st
( i = 0 & i in X & ( for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies 0 = 0 ) ) by A1; :: thesis:

end;

suppose A2: X <> {} ; :: thesis:

then reconsider X9 = X as non empty finite Subset of NAT ;
deffunc H₁( Element of X9) -> Element of REAL = f /. ((2 * n) + $1);
consider x being Element of X9 such that
A3: for y being Element of X9 holds H₁(x) <= H₁(y) from PRE_CIRC:sch 5();
reconsider x = x as Element of NAT ;
defpred S₁[ Nat] means ( $1 in X & f /. ((2 * n) + x) = f /. ((2 * n) + $1) );
A4: ex i being Nat st S₁[i] ;
consider i being Nat such that
A5: ( S₁[i] & ( for k being Nat st S₁[k] holds
i <= k ) ) from NAT_1:sch 5(A4);
take F = i; :: thesis:

hereby :: thesis:

assume X <> {} ; :: thesis:
take i = F; :: thesis:
thus ( i = F & i in X ) by A5; :: thesis:
thus for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) by A3, A5; :: thesis:
thus for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k by A5; :: thesis:

end;

thus ( X = {} implies F = 0 ) by A2; :: thesis:

end;