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;
A9: L1 c= NAT * by A8, XBOOLE_1:1;
A10: L2 c= NAT * by A8, XBOOLE_1:1;

A11: 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
reconsider p = x as FinSequence of NAT by A9, A12, FINSEQ_1:def 11;
A13: for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) by A6, A12;
thus x in L2 by A7, A12, A13; :: thesis: verum

end;

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

end;

thus L1 = L2 by A11, TARSKI:2; :: thesis: verum