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