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