let T1, T2 be DTree-set of D; :: thesis: ( ( for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in T1 ) ) & ( for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in T2 ) ) implies T1 = T2 )
assume that
A3: for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in T1 ) and
A4: for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in T2 ) ; :: thesis: T1 = T2
thus T1 c= T2 :: according to XBOOLE_0:def 10 :: thesis: T2 c= T1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T1 or x in T2 )
assume A5: x in T1 ; :: thesis: x in T2
then reconsider T = x as DecoratedTree of D ;
( dom T is finite & T is binary ) by A3, A5;
hence x in T2 by A4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T2 or x in T1 )
assume A6: x in T2 ; :: thesis: x in T1
then reconsider T = x as DecoratedTree of D ;
( dom T is finite & T is binary ) by A4, A6;
hence x in T1 by A3; :: thesis: verum