given i, j being Nat such that A3:
i indom p
and A4:
( j indom p & i <> j )
and
p . i = j
and
p . j = i
and A5:
for k being Nat st k <> i & k <> j & k indom p holds p . k = k
; :: thesis: contradiction
ex k being Element of NAT st ( k <> i & k <> j & k indom p )