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
A41: 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
A42: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in S1 or x in S2 )
assume A43: x in S1 ; :: thesis: x in S2
then reconsider q = x as FinSequence of NAT by Th18;
( ( 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 A41, A43;
hence x in S2 by A42; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S2 or x in S1 )
assume A44: x in S2 ; :: thesis: x in S1
then reconsider q = x as FinSequence of NAT by Th18;
( ( 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 A42, A44;
hence x in S1 by A41; :: thesis: verum