theorem Th14: :: HILBERT4:6

for x being set
for V being SetValuation
for P being Permutation of V
for p, q being Element of HP-WFF st x is_a_fixpoint_of Perm (P,q) holds
(SetVal (V,p)) --> x is_a_fixpoint_of Perm (P,(p => q))