let X be non empty constituted-DTrees set ; :: thesis: for t being DecoratedTree st t in X holds
Subtrees t c= Subtrees X
let t be DecoratedTree; :: thesis: ( t in X implies Subtrees t c= Subtrees X )
assume A1: t in X ; :: thesis: Subtrees t c= Subtrees X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Subtrees t or x in Subtrees X )
assume x in Subtrees t ; :: thesis: x in Subtrees X
then consider p being Element of dom t such that
A2: x = t | p ;
thus x in Subtrees X by A1, A2; :: thesis: verum