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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } or x in Subtrees t )
assume x in { (t | p) where p is Node of t : ( not p in Leaves (dom t) or t . p in C ) } ; :: thesis: x in Subtrees t
then 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 t ; :: thesis: verum

end;

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