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