let T be Tree; :: thesis: T is T-Substitution of 0
let t be Element of T; :: according to TREES_3:def 14 :: thesis: ( t in elementary_tree 0 or ex l being Leaf of elementary_tree 0 st l is_a_proper_prefix_of t )
assume A1: not t in elementary_tree 0 ; :: thesis: ex l being Leaf of elementary_tree 0 st l is_a_proper_prefix_of t
set l = the Leaf of elementary_tree 0;
take the Leaf of elementary_tree 0 ; :: thesis: the Leaf of elementary_tree 0 is_a_proper_prefix_of t
A2: the Leaf of elementary_tree 0 = {} by TARSKI:def 1, TREES_1:29;
A3: t <> {} by A1, TARSKI:def 1, TREES_1:29;
{} is_a_prefix_of t ;
hence the Leaf of elementary_tree 0 is_a_proper_prefix_of t by A2, A3; :: thesis: verum