let n, k be Element of NAT ; :: thesis: ( n <= k implies dyadic n c= dyadic k )
assume A1: n <= k ; :: thesis: dyadic n c= dyadic k
A2: for s being Element of NAT holds dyadic n c= dyadic (n + s)

proof

defpred S₁[ Element of NAT ] means dyadic n c= dyadic (n + $1);
A3: S₁[ 0 ] ;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: dyadic n c= dyadic (n + k) ; :: thesis: S₁[k + 1]
dyadic (n + k) c= dyadic ((n + k) + 1) by URYSOHN1:11;
hence S₁[k + 1] by A5, XBOOLE_1:1; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
hence for s being Element of NAT holds dyadic n c= dyadic (n + s) ; :: thesis: verum

end;

consider s being Nat such that
A6: k = n + s by A1, NAT_1:10;
s in NAT by ORDINAL1:def 13;
hence dyadic n c= dyadic k by A2, A6; :: thesis: verum