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

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