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