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
consider l being Leaf of elementary_tree 0 ;
take l ; :: thesis: l is_a_proper_prefix_of t
A2: l = {} by TARSKI:def 1, TREES_1:56;
A3: t <> {} by A1, TARSKI:def 1, TREES_1:56;
{} is_a_prefix_of t by XBOOLE_1:2;
hence l is_a_proper_prefix_of t by A2, A3, XBOOLE_0:def 8; :: thesis: verum