let x be set ; :: thesis: derangements {x} = {}
A1: card {x} = 1 by CARD_1:50;
1 / number_e < 1 / 2 by XREAL_1:78, TAYLOR_1:11;
then - (1 / 2) < - (1 / number_e) by XREAL_1:26;
then |.(0 - (1 / number_e)).| < 1 / 2 by SEQ_2:9;
then round (1 / number_e) = 0 by RoundCorrect;
then card (derangements {x}) = 0 by Th4, A1, NEWTON:19;
hence derangements {x} = {} ; :: thesis: verum