let T1, T2 be Tree; :: thesis: ( ( for n being Nat holds T1 -level n = T2 -level n ) implies T1 = T2 )
assume A1: for n being Nat holds T1 -level n = T2 -level n ; :: thesis: T1 = T2
for p being FinSequence of NAT holds
( p in T1 iff p in T2 )

proof

let p be FinSequence of NAT ; :: thesis: ( p in T1 iff p in T2 )
A2: T1 = union { (T1 -level n) where n is Nat : verum } by Th14;

hereby :: thesis: ( p in T2 implies p in T1 )

assume p in T1 ; :: thesis: p in T2
then consider Y being set such that
A3: p in Y and
A4: Y in { (T1 -level n) where n is Nat : verum } by A2, TARSKI:def 4;
consider n being Nat such that
A5: Y = T1 -level n by A4;
Y = T2 -level n by A1, A5;
hence p in T2 by A3; :: thesis: verum

end;

assume A6: p in T2 ; :: thesis: p in T1
T2 = union { (T2 -level n) where n is Nat : verum } by Th14;
then consider Y being set such that
A7: p in Y and
A8: Y in { (T2 -level n) where n is Nat : verum } by A6, TARSKI:def 4;
consider n being Nat such that
A9: Y = T2 -level n by A8;
Y = T1 -level n by A1, A9;
hence p in T1 by A7; :: thesis: verum

end;

hence T1 = T2 ; :: thesis: verum