let d1, d2 be Dyadic; :: thesis: ( d1 < d2 iff uDyadic . d1 < uDyadic . d2 )
consider i1 being Integer, n1 being Nat such that
A1: d1 = i1 / (2 |^ n1) by Th18;
consider i2 being Integer, n2 being Nat such that
A2: d2 = i2 / (2 |^ n2) by Th18;
(2 |^ n1) * (2 |^ n2) = 2 |^ (n1 + n2) by NEWTON:8;
then A3: ( d1 = (i1 * (2 |^ n2)) / (2 |^ (n1 + n2)) & d2 = (i2 * (2 |^ n1)) / (2 |^ (n1 + n2)) ) by A1, A2, XCMPLX_1:91;
thus ( d1 < d2 implies uDyadic . d1 < uDyadic . d2 ) :: thesis: ( uDyadic . d1 < uDyadic . d2 implies d1 < d2 )

proof

assume d1 < d2 ; :: thesis: uDyadic . d1 < uDyadic . d2
then i1 * (2 |^ n2) < i2 * (2 |^ n1) by A3, XREAL_1:72;
hence uDyadic . d1 < uDyadic . d2 by A3, Lm5; :: thesis: verum

end;

assume uDyadic . d1 < uDyadic . d2 ; :: thesis: d1 < d2
then i1 * (2 |^ n2) < i2 * (2 |^ n1) by A3, Lm5;
hence d1 < d2 by A3, XREAL_1:74; :: thesis: verum