( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def 2;
hence ( 0 in the Symbols of SumTuring & 1 in the Symbols of SumTuring ) by Def14; :: thesis: verum