let D1, D2 be Subset of DYADIC; :: thesis: ( ( for d being Dyadic holds
( d in D1 iff ex i being Integer st d = i / (2 |^ n) ) ) & ( for d being Dyadic holds
( d in D2 iff ex i being Integer st d = i / (2 |^ n) ) ) implies D1 = D2 )
assume that
A3: for d being Dyadic holds
( d in D1 iff ex i being Integer st d = i / (2 |^ n) ) and
A4: for d being Dyadic holds
( d in D2 iff ex i being Integer st d = i / (2 |^ n) ) ; :: thesis: D1 = D2
thus D1 c= D2 :: according to XBOOLE_0:def 10 :: thesis: D2 c= D1

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in D1 or o in D2 )
assume o in D1 ; :: thesis: o in D2
then ex i being Integer st o = i / (2 |^ n) by A3;
hence o in D2 by A4; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in D2 or o in D1 )
assume o in D2 ; :: thesis: o in D1
then ex i being Integer st o = i / (2 |^ n) by A4;
hence o in D1 by A3; :: thesis: verum