let s be non empty finite set ; :: thesis: card (derangements s) = round (((card s) !) / number_e)
|.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 by Th3;
hence card (derangements s) = round (((card s) !) / number_e) by RoundCorrect; :: thesis: verum