let S1, S2 be Tree; :: thesis: ( ( for q being FinSequence of NAT holds
( q in S1 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds
( q in S2 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ) implies S1 = S2 )
assume that
A124: for q being FinSequence of NAT holds
( q in S1 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) and
A125: for q being FinSequence of NAT holds
( q in S2 iff ( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) ) ; :: thesis: S1 = S2
let x be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not x in S1 or x in S2 ) & ( not x in S2 or x in S1 ) )
thus ( x in S1 implies x in S2 ) :: thesis: ( not x in S2 or x in S1 )

proof

assume A126: x in S1 ; :: thesis: x in S2
reconsider q = x as FinSequence of NAT ;
( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) by A124, A126;
hence x in S2 by A125; :: thesis: verum

end;

assume A128: x in S2 ; :: thesis: x in S1
reconsider q = x as FinSequence of NAT ;
( ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) ) by A125, A128;
hence x in S1 by A124; :: thesis: verum