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

proof

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

end;

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