let T1, T2 be DTree-set of D; :: thesis: ( ( for T being DecoratedTree of D holds T in T1 ) & ( for T being DecoratedTree of D holds T in T2 ) implies T1 = T2 )
assume that
A8: for T being DecoratedTree of D holds T in T1 and
A9: for T being DecoratedTree of D holds T in T2 ; :: thesis: T1 = T2
thus T1 c= T2 by A9; :: according to XBOOLE_0:def 10 :: thesis: T2 c= T1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T2 or x in T1 )
thus ( not x in T2 or x in T1 ) by A8; :: thesis: verum