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

let x be object ; :: thesis: ( x in derangements {} implies x in {{}} )
assume x in derangements {} ; :: thesis: x in {{}}
then ex f being Permutation of {} st
( x = f & f is without_fixpoints ) ;
hence x in {{}} by FUNCT_2:9, FUNCT_2:127; :: thesis: verum

end;

let x be object ; :: 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:57;
hence x in derangements {} by A1, Th1; :: thesis: verum