let s be Element of T with-replacement (t,S); :: according to TREES_3:def 14 :: thesis: ( s in T or ex l being Leaf of T st l is_a_proper_prefix_of s )
assume A1: not s in T ; :: thesis: ex l being Leaf of T st l is_a_proper_prefix_of s
then consider t1 being FinSequence of NAT such that
t1 in S and
A2: s = t ^ t1 by TREES_1:def 9;
take t ; :: thesis: t is_a_proper_prefix_of s
t ^ {} = t by FINSEQ_1:34;
then t1 <> {} by A1, A2;
hence t is_a_proper_prefix_of s by A2, TREES_1:10; :: thesis: verum