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