let L1, L2 be Subset of T; :: thesis: ( ( for p being FinSequence of NAT holds
( p in L1 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) & ( for p being FinSequence of NAT holds
( p in L2 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) implies L1 = L2 )
assume that
A6: for p being FinSequence of NAT holds
( p in L1 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) and
A7: for p being FinSequence of NAT holds
( p in L2 iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ; :: thesis: L1 = L2
A8: T c= NAT * by Def5;
then A9: L1 c= NAT * by XBOOLE_1:1;
A10: L2 c= NAT * by A8, XBOOLE_1:1;

now

let x be set ; :: thesis: ( ( x in L1 implies x in L2 ) & ( x in L2 implies x in L1 ) )
thus ( x in L1 implies x in L2 ) :: thesis: ( x in L2 implies x in L1 )

proof

assume A12: x in L1 ; :: thesis: x in L2
then reconsider p = x as FinSequence of NAT by A9, FINSEQ_1:def 11;
for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) by A6, A12;
hence x in L2 by A7, A12; :: thesis: verum

end;

assume A14: x in L2 ; :: thesis: x in L1
then reconsider p = x as FinSequence of NAT by A10, FINSEQ_1:def 11;
for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) by A7, A14;
hence x in L1 by A6, A14; :: thesis: verum

end;

hence L1 = L2 by TARSKI:2; :: thesis: verum