thus ( s is increasing implies for n being Nat holds s . n < s . (n + 1) ) :: thesis: ( ( for n being Nat holds s . n < s . (n + 1) ) implies s is increasing )
proof
assume A1: s is increasing ; :: thesis: for n being Nat holds s . n < s . (n + 1)
let n be Nat; :: thesis: s . n < s . (n + 1)
A2: n < n + 1 by NAT_1:13;
( dom s = NAT & n in NAT ) by FUNCT_2:def 1, ORDINAL1:def 12;
hence s . n < s . (n + 1) by A1, A2; :: thesis: verum
end;
assume A3: for n being Nat holds s . n < s . (n + 1) ; :: thesis: s is increasing
let e1 be ExtReal; :: according to VALUED_0:def 13 :: thesis: for b1 being object holds
( not e1 in dom s or not b1 in dom s or b1 <= e1 or not s . b1 <= s . e1 )
let e2 be ExtReal; :: thesis: ( not e1 in dom s or not e2 in dom s or e2 <= e1 or not s . e2 <= s . e1 )
assume ( e1 in dom s & e2 in dom s ) ; :: thesis: ( e2 <= e1 or not s . e2 <= s . e1 )
then reconsider m = e1, n = e2 as Nat ;
defpred S1[ Nat] means ( m < $1 implies s . m < s . $1 );
A4: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume A5: S1[j] ; :: thesis: S1[j + 1]
assume m < j + 1 ; :: thesis: s . m < s . (j + 1)
then m <= j by NAT_1:13;
then ( s . m < s . j or m = j ) by A5, XXREAL_0:1;
hence s . m < s . (j + 1) by A3, XXREAL_0:2; :: thesis: verum
end;
assume A6: e1 < e2 ; :: thesis: not s . e2 <= s . e1
A7: S1[ 0 ] ;
for j being Nat holds S1[j] from NAT_1:sch 2(A7, A4);
 then s . m < s . n by A6;
hence not s . e2 <= s . e1 ; :: thesis: verum