theorem :: MOD_4:26

for K being Skew-Field holds
( id K is antiisomorphism iff K is Field )