A1: for x being Element of Permutations F₁() st x in F₂() holds
P₁[{x}] and
A2: for x being Element of Permutations F₁()
for B being non empty Element of Fin (Permutations F₁()) st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[B \/ {x}]