let p be Element of HP-WFF ; :: thesis: ( p is canonical implies p is pseudo-canonical )

assume A1: p is canonical ; :: thesis: p is pseudo-canonical

let V be SetValuation; :: according to HILBERT3:def 8 :: thesis: for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p)

consider x being set such that

A2: for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p) by A1;

let P be Permutation of V; :: thesis: ex x being set st x is_a_fixpoint_of Perm (P,p)

take x ; :: thesis: x is_a_fixpoint_of Perm (P,p)

thus x is_a_fixpoint_of Perm (P,p) by A2; :: thesis: verum

assume A1: p is canonical ; :: thesis: p is pseudo-canonical

let V be SetValuation; :: according to HILBERT3:def 8 :: thesis: for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,p)

consider x being set such that

A2: for P being Permutation of V holds x is_a_fixpoint_of Perm (P,p) by A1;

let P be Permutation of V; :: thesis: ex x being set st x is_a_fixpoint_of Perm (P,p)

take x ; :: thesis: x is_a_fixpoint_of Perm (P,p)

thus x is_a_fixpoint_of Perm (P,p) by A2; :: thesis: verum