let n, m be Nat; :: thesis: ( n <= m implies DYADIC n c= DYADIC m )
assume n <= m ; :: thesis: DYADIC n c= DYADIC m
then reconsider mn = m - n as Nat by NAT_1:21;
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in DYADIC n or o in DYADIC m )
assume A1: o in DYADIC n ; :: thesis: o in DYADIC m
then reconsider o = o as Dyadic ;
consider i being Integer such that
A2: o = i / (2 |^ n) by A1, Def4;
A3: (2 |^ n) * (2 |^ mn) = 2 |^ (n + mn) by NEWTON:8;
o = (i * (2 |^ mn)) / ((2 |^ n) * (2 |^ mn)) by A2, XCMPLX_1:91;
hence o in DYADIC m by A3, Def4; :: thesis: verum