let C be set ; :: thesis: for X being non empty constituted-DTrees set holds C -Subtrees X = union { (C -Subtrees t) where t is Element of X : verum }
let X be non empty constituted-DTrees set ; :: thesis: C -Subtrees X = union { (C -Subtrees t) where t is Element of X : verum }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (C -Subtrees t) where t is Element of X : verum } c= C -Subtrees X

let x be set ; :: thesis: ( x in C -Subtrees X implies x in union { (C -Subtrees s) where s is Element of X : verum } )
assume x in C -Subtrees X ; :: thesis: x in union { (C -Subtrees s) where s is Element of X : verum }
then consider t being Element of X such that
A1: ex n being Node of t st
( x = t | n & ( not n in Leaves (dom t) or t . n in C ) ) ;
( C -Subtrees t in { (C -Subtrees s) where s is Element of X : verum } & x in C -Subtrees t ) by A1;
hence x in union { (C -Subtrees s) where s is Element of X : verum } by TARSKI:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (C -Subtrees t) where t is Element of X : verum } or x in C -Subtrees X )
assume x in union { (C -Subtrees s) where s is Element of X : verum } ; :: thesis: x in C -Subtrees X
then consider Y being set such that
A2: x in Y and
A3: Y in { (C -Subtrees s) where s is Element of X : verum } by TARSKI:def 4;
consider t being Element of X such that
A4: Y = C -Subtrees t by A3;
ex p being Node of t st
( x = t | p & ( not p in Leaves (dom t) or t . p in C ) ) by A2, A4;
hence x in C -Subtrees X ; :: thesis: verum