(1. (K,n)) @ = 1. (K,n) by Th10;
hence 1. (K,n) is symmetric by Def5; :: thesis: verum