[(1. K),(1. K),(1. K)] <> [(0. K),(0. K),(0. K)] by XTUPLE_0:3;
then not [(1. K),(1. K),(1. K)] in {[(0. K),(0. K),(0. K)]} by TARSKI:def 1;
hence [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]} is non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:] by XBOOLE_0:def 5; :: thesis: verum