take (n,n) --> (0. K) ; :: thesis: (n,n) --> (0. K) is subsymmetric
thus (n,n) --> (0. K) is subsymmetric ; :: thesis: verum