let V be SetValuation; :: thesis: for P being Permutation of V
for p, q being Element of HP-WFF st Perm (P,q) is with_fixpoint holds
Perm (P,(p => q)) is with_fixpoint
let P be Permutation of V; :: thesis: for p, q being Element of HP-WFF st Perm (P,q) is with_fixpoint holds
Perm (P,(p => q)) is with_fixpoint
let p, q be Element of HP-WFF ; :: thesis: ( Perm (P,q) is with_fixpoint implies Perm (P,(p => q)) is with_fixpoint )
given x being object such that A1: x is_a_fixpoint_of Perm (P,q) ; :: according to ABIAN:def 5 :: thesis: Perm (P,(p => q)) is with_fixpoint
reconsider xx = x as set by TARSKI:1;
take (SetVal (V,p)) --> xx ; :: according to ABIAN:def 5 :: thesis: (SetVal (V,p)) --> xx is_a_fixpoint_of Perm (P,(p => q))
thus (SetVal (V,p)) --> xx is_a_fixpoint_of Perm (P,(p => q)) by A1, Th14; :: thesis: verum