ex T being Tree st
for p being FinSequence holds
( p in T iff ( p in F₁() or ex q being Element of F₁() ex r being Element of F₂() st
( P₁[q] & p = q ^ r ) ) )