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
A4: 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
A5: 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
A6: T c= NAT * by Def3;
then A7: L1 c= NAT * ;
A8: L2 c= NAT * by A6;

now :: thesis: for x being object holds
( ( x in L1 implies x in L2 ) & ( x in L2 implies x in L1 ) )

let x be object ; :: 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 A9: x in L1 ; :: thesis: x in L2
then reconsider p = x as FinSequence of NAT by A7, 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 A4, A9;
hence x in L2 by A5, A9; :: thesis: verum

end;

assume A10: x in L2 ; :: thesis: x in L1
then reconsider p = x as FinSequence of NAT by A8, 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 A5, A10;
hence x in L1 by A4, A10; :: thesis: verum

end;

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