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