let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in t1 with-replacement ((<*> NAT),t) or p in t ) & ( not p in t or p in t1 with-replacement ((<*> NAT),t) ) )
A3: {} in t1 by TREES_1:22;
then A2: ( p in t1 with-replacement ((<*> NAT),t) iff ( ( p in t1 & not {} is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in t & p = {} ^ r ) ) ) by TREES_1:def 9;
hereby :: thesis: ( not p in t or p in t1 with-replacement ((<*> NAT),t) )
assume p in t1 with-replacement ((<*> NAT),t) ; :: thesis: p in t
per cases then ( {} = p or ex r being FinSequence of NAT st
( r in t & p = {} ^ r ) ) by A2, XBOOLE_1:61;
suppose ex r being FinSequence of NAT st
( r in t & p = {} ^ r ) ; :: thesis: p in t
hence p in t ; :: thesis: verum
end;
end;
end;
assume p in t ; :: thesis: p in t1 with-replacement ((<*> NAT),t)
then ( p in t & p = {} ^ p ) ;
hence p in t1 with-replacement ((<*> NAT),t) by A3, TREES_1:def 9; :: thesis: verum