( 0 in {0 ,1} & 1 in {0 ,1} ) by TARSKI:def 2;
hence ( 0 in the Symbols of U3(n)Turing & 1 in the Symbols of U3(n)Turing ) by Def22; :: thesis: verum