let S1, S2 be Tree; :: thesis: ( ( for q being FinSequence of NAT holds
( q in S1 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds
( q in S2 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) ) implies S1 = S2 )
assume that
A94: for q being FinSequence of NAT holds
( q in S1 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) and
A95: for q being FinSequence of NAT holds
( q in S2 iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ) ; :: thesis: S1 = S2
thus S1 c= S2 :: according to XBOOLE_0:def 10 :: thesis: S2 is_a_prefix_of S1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in S1 or x in S2 )
assume A96: x in S1 ; :: thesis: x in S2
reconsider q = x as FinSequence of NAT by A96, Th44;
A97: ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) by A94, A96;
thus x in S2 by A95, A97; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in S2 or x in S1 )
assume A98: x in S2 ; :: thesis: x in S1
reconsider q = x as FinSequence of NAT by A98, Th44;
A99: ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) by A95, A98;
thus x in S1 by A94, A99; :: thesis: verum