let x be object ; :: thesis: derangements {x} = {}
A1: card {x} = 1 by CARD_1:30;
1 / number_e < 1 / 2 by TAYLOR_1:11, XREAL_1:76;
then - (1 / 2) < - (1 / number_e) by XREAL_1:24;
then |.(0 - (1 / number_e)).| < 1 / 2 by SEQ_2:1;
then round (1 / number_e) = 0 by Th4;
then card (derangements {x}) = 0 by Th10, A1, NEWTON:13;
hence derangements {x} = {} ; :: thesis: verum