let D1, D2 be DTree-set 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 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 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 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 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 object ; :: 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 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 object ; :: 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 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