let D1, D2 be DOMAIN_DecoratedTree of [:NAT ,NAT :]; :: thesis: ( ( for x being DecoratedTree of [:NAT ,NAT :] st x in D1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT ,NAT :] holds
( x in D1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) & ( for x being DecoratedTree of [:NAT ,NAT :] st x in D2 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT ,NAT :] holds
( x in D2 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) implies D1 = D2 )
assume that
A12: for x being DecoratedTree of [:NAT ,NAT :] st x in D1 holds
x is finite and
A13: for x being finite DecoratedTree of [:NAT ,NAT :] holds
( x in D1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) and
A14: for x being DecoratedTree of [:NAT ,NAT :] st x in D2 holds
x is finite and
A15: for x being finite DecoratedTree of [:NAT ,NAT :] holds
( x in D2 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ; :: thesis: D1 = D2
thus D1 c= D2 :: according to XBOOLE_0:def 10 :: thesis: D2 c= D1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 or x in D2 )
assume A16: x in D1 ; :: thesis: x in D2
reconsider y = x as finite DecoratedTree of [:NAT ,NAT :] by A12, A16;
for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) by A13, A16;
hence x in D2 by A15; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D2 or x in D1 )
assume A17: x in D2 ; :: thesis: x in D1
reconsider y = x as finite DecoratedTree of [:NAT ,NAT :] by A14, A17;
for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) by A15, A17;
hence x in D1 by A13; :: thesis: verum