:: deftheorem defines derangements CARDFIN2:def 2 :
for s being set holds derangements s = { f where f is Permutation of s : f is without_fixpoints } ;