let T1, T2 be Tree; :: thesis:
assume that
A23: for q being FinSequence of NAT holds
( q in T1 iff p ^ q in T ) and
A24: for q being FinSequence of NAT holds
( q in T2 iff p ^ q in T ) ; :: thesis:

let x be object ; :: thesis:
thus ( x in T1 implies x in T2 ) :: thesis:

assume A25: x in T1 ; :: thesis:
then reconsider q = x as FinSequence of NAT by Th18;
p ^ q in T by A23, A25;
hence x in T2 by A24; :: thesis:

end;

assume A26: x in T2 ; :: thesis:
then reconsider q = x as FinSequence of NAT by Th18;
p ^ q in T by A24, A26;
hence x in T1 by A23; :: thesis:

end;