set W = { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ;
{ (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } c= Subtrees X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } or x in Subtrees X )
assume x in { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ; :: thesis: x in Subtrees X
then ex t being Element of X ex p being Node of t st
( x = t | p & ( not p in Leaves (dom t) or t . p in C ) ) ;
hence x in Subtrees X ; :: thesis: verum

end;

hence { (t | p) where t is Element of X, p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } is Subset of (Subtrees X) ; :: thesis: verum