hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: {{} } c= derangements {}

let x be set ; :: thesis: ( x in derangements {} implies x in {{} } )
assume x in derangements {} ; :: thesis: x in {{} }
then ex f being Permutation of {} st
( x = f & f has_no_fixpoint ) ;
hence x in {{} } by RELAT_1:81, ALTCAT_1:3, FUNCT_2:12; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in derangements {} )
assume x in {{} } ; :: thesis: x in derangements {}
then A1: x = {} by TARSKI:def 1;
rng (id {} ) = {} ;
then id {} is Permutation of {} by FUNCT_2:83;
hence x in derangements {} by A1, IdNoFix; :: thesis: verum