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
A1: SetVal V,VERUM = 1 by Def2;
0 in 1 by CARD_1:87, TARSKI:def 1;
hence 0 is_a_fixpoint_of Perm P,VERUM by A1, Th3, CARD_1:87; :: thesis: verum