theorem Th26: :: HILBERT3:27

for A, B being non empty set
for P being Permutation of A
for Q being Permutation of B holds (P => Q) " = (P ") => (Q ")