:: deftheorem defines canonical HILBERT3:def 7 :
for p being Element of HP-WFF holds
( p is canonical iff for V being SetValuation ex x being set st
for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p) );