take T ; :: thesis: 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 )
thus 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 ) ; :: thesis: verum