let n, k be Nat; :: thesis: ( n <= k implies dyadic n c= dyadic k )
A1: for s being Nat holds dyadic n c= dyadic (n + s)

proof

defpred S₁[ Nat] means dyadic n c= dyadic (n + $1);
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A3: dyadic (n + k) c= dyadic ((n + k) + 1) by URYSOHN1:5;
assume dyadic n c= dyadic (n + k) ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A3, XBOOLE_1:1; :: thesis: verum

end;

A4: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
hence for s being Nat holds dyadic n c= dyadic (n + s) ; :: thesis: verum

end;

assume n <= k ; :: thesis: dyadic n c= dyadic k
then consider s being Nat such that
A5: k = n + s by NAT_1:10;
thus dyadic n c= dyadic k by A1, A5; :: thesis: verum