let x be Element of Subtrees t; :: thesis: x is finite
x in { (t | p) where p is Node of t : verum } ;
then ex p being Node of t st x = t | p ;
hence x is finite ; :: thesis: verum