let T1, T2 be Tree; :: thesis: ( ( for q being FinSequence of NAT holds
( q in T1 iff p ^ q in T ) ) & ( for q being FinSequence of NAT holds
( q in T2 iff p ^ q in T ) ) implies T1 = T2 )
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: T1 = T2

now :: thesis: for x being object holds
( ( x in T1 implies x in T2 ) & ( x in T2 implies x in T1 ) )

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

proof

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

end;

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

end;

hence T1 = T2 by TARSKI:2; :: thesis: verum