take the non empty symmetric with_fixpoint Permutation of the non empty set ; :: thesis: ( the non empty symmetric with_fixpoint Permutation of the non empty set is with_fixpoint & not the non empty symmetric with_fixpoint Permutation of the non empty set is empty & the non empty symmetric with_fixpoint Permutation of the non empty set is symmetric )
thus ( the non empty symmetric with_fixpoint Permutation of the non empty set is with_fixpoint & not the non empty symmetric with_fixpoint Permutation of the non empty set is empty & the non empty symmetric with_fixpoint Permutation of the non empty set is symmetric ) ; :: thesis: verum