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 )
proof
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;
assume A57: 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 A55, A57;
hence x in S1 by A54; :: thesis: verum