theorem Lm3: :: HILBERT4:8

for V being SetValuation
for P being Permutation of V
for p, q being Element of HP-WFF st Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints holds
Perm (P,(p => q)) is without_fixpoints