let T, T9 be Tree; :: thesis: for p being FinSequence of NAT st p in Leaves T holds
T c= T with-replacement (p,T9)
let p be FinSequence of NAT ; :: thesis: ( p in Leaves T implies T c= T with-replacement (p,T9) )
assume A1: p in Leaves T ; :: thesis: T c= T with-replacement (p,T9)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in T with-replacement (p,T9) )
assume x in T ; :: thesis: x in T with-replacement (p,T9)
then reconsider t = x as Element of T ;
not p is_a_proper_prefix_of t by A1, TREES_1:def 5;
hence x in T with-replacement (p,T9) by A1, TREES_1:def 9; :: thesis: verum