set P = permutations {};
thus permutations {} c= 1 :: according to XBOOLE_0:def 10 :: thesis: 1 c= permutations {}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in permutations {} or x in 1 )
assume x in permutations {} ; :: thesis: x in 1
then x is Permutation of {} by Th1;
hence x in 1 by CARD_1:49, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in 1 or x in permutations {} )
assume x in 1 ; :: thesis: x in permutations {}
then x = {} ({},{}) by CARD_1:49, TARSKI:def 1;
hence x in permutations {} ; :: thesis: verum