let n, k be Nat; :: thesis: ( k <= n implies Triangle k <= Triangle n )
assume k <= n ; :: thesis: Triangle k <= Triangle n
then consider i being Nat such that
A1: n = k + i by NAT_1:10;
defpred S₁[ Nat] means for n being Nat holds Triangle n <= Triangle (n + $1);
A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let n be Nat; :: thesis: Triangle n <= Triangle (n + (k + 1))
A5: Triangle n <= Triangle (n + k) by A4;
Triangle (n + k) <= Triangle ((n + k) + 1) by Th42;
hence Triangle n <= Triangle (n + (k + 1)) by A5, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence Triangle k <= Triangle n by A1; :: thesis: verum