theorem Th18: :: MATRIX11:18

for X being set
for x being object st not x in X holds
for p1 being Permutation of (X \/ {x}) st p1 . x = x holds
ex p being Permutation of X st p1 | X = p