:: deftheorem Def2 defines ProperPrefixes TREES_1:def 2 :
for p being FinSequence
for b₂ being set holds
( b₂ = ProperPrefixes p iff for x being object holds
( x in b₂ iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) );