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

A54: 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

A55: 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 )

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 A55, A57;

hence x in S1 by A54; :: thesis: verum

( 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

A54: 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

A55: 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 A57:
x in S2
; :: thesis: x in S1
assume A56:
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 A54, A56;

hence x in S2 by A55; :: thesis: verum

end;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 A54, A56;

hence x in S2 by A55; :: thesis: verum

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 A55, A57;

hence x in S1 by A54; :: thesis: verum