let X, f be set ; :: thesis: ( f in permutations X implies f is Permutation of X )
assume f in permutations X ; :: thesis: f is Permutation of X
then ex g being Permutation of X st g = f ;
hence f is Permutation of X ; :: thesis: verum