let V be SetValuation; :: according to HILBERT3:def 7 :: thesis: ex x being set st

for P being Permutation of V holds x is_a_fixpoint_of Perm (P,VERUM)

take 0 ; :: thesis: for P being Permutation of V holds 0 is_a_fixpoint_of Perm (P,VERUM)

let P be Permutation of V; :: thesis: 0 is_a_fixpoint_of Perm (P,VERUM)

( SetVal (V,VERUM) = 1 & 0 in 1 ) by Def2, CARD_1:49, TARSKI:def 1;

hence 0 is_a_fixpoint_of Perm (P,VERUM) by Th3, CARD_1:49; :: thesis: verum

for P being Permutation of V holds x is_a_fixpoint_of Perm (P,VERUM)

take 0 ; :: thesis: for P being Permutation of V holds 0 is_a_fixpoint_of Perm (P,VERUM)

let P be Permutation of V; :: thesis: 0 is_a_fixpoint_of Perm (P,VERUM)

( SetVal (V,VERUM) = 1 & 0 in 1 ) by Def2, CARD_1:49, TARSKI:def 1;

hence 0 is_a_fixpoint_of Perm (P,VERUM) by Th3, CARD_1:49; :: thesis: verum