set seq = incl NAT ;

now

let n be Element of NAT ; :: thesis: (incl NAT ) . n < (incl NAT ) . (n + 1)
( (incl NAT ) . n = n & (incl NAT ) . (n + 1) = n + 1 ) by FUNCT_1:35;
hence (incl NAT ) . n < (incl NAT ) . (n + 1) by NAT_1:13; :: thesis: verum

end;

hence ( incl NAT is increasing & incl NAT is natural-valued ) by Lm6; :: thesis: verum