let W, W1 be Tree; :: thesis: for p, q being FinSequence of NAT st p in W & q in W & not p is_a_prefix_of q holds
q in W with-replacement p,W1
let p, q be FinSequence of NAT ; :: thesis: ( p in W & q in W & not p is_a_prefix_of q implies q in W with-replacement p,W1 )
( not p is_a_prefix_of q implies not p is_a_proper_prefix_of q ) by XBOOLE_0:def 8;
hence ( p in W & q in W & not p is_a_prefix_of q implies q in W with-replacement p,W1 ) by TREES_1:def 12; :: thesis: verum