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