for t being Element of T holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) ;
then T is T-Substitution of T by Def14;
hence ex b₁ being T-Substitution of T st b₁ is finite ; :: thesis: verum