let p, q be Element of HP-WFF ; :: thesis: 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

let V be SetValuation; :: thesis: 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

let P be Permutation of V; :: thesis: ( 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) ) implies not p => q is pseudo-canonical )

given x being set such that A1: x is_a_fixpoint_of Perm (P,p) ; :: thesis: ( ex f being set st f is_a_fixpoint_of Perm (P,q) or not p => q is pseudo-canonical )

assume A2: for x being set holds not x is_a_fixpoint_of Perm (P,q) ; :: thesis: not p => q is pseudo-canonical

assume p => q is pseudo-canonical ; :: thesis: contradiction

then consider f being set such that

A3: f is_a_fixpoint_of Perm (P,(p => q)) ;

reconsider f = f as Function by A3;

f . x is_a_fixpoint_of Perm (P,q) by A1, A3, Th39;

hence contradiction by A2; :: thesis: verum

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

let V be SetValuation; :: thesis: 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

let P be Permutation of V; :: thesis: ( 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) ) implies not p => q is pseudo-canonical )

given x being set such that A1: x is_a_fixpoint_of Perm (P,p) ; :: thesis: ( ex f being set st f is_a_fixpoint_of Perm (P,q) or not p => q is pseudo-canonical )

assume A2: for x being set holds not x is_a_fixpoint_of Perm (P,q) ; :: thesis: not p => q is pseudo-canonical

assume p => q is pseudo-canonical ; :: thesis: contradiction

then consider f being set such that

A3: f is_a_fixpoint_of Perm (P,(p => q)) ;

reconsider f = f as Function by A3;

f . x is_a_fixpoint_of Perm (P,q) by A1, A3, Th39;

hence contradiction by A2; :: thesis: verum