for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm (P,p) & ( for f being set holds not f is_a_fixpoint_of Perm (P,q) ) holds
not p => q is pseudo-canonical