reconsider x = Head s as Element of INT ;
the Tran of T . [(s `1_3),((s `3_3) . x)] is Tran-Goal of T ;
hence the Tran of T . [(s `1_3),((s `3_3) . (Head s))] is Tran-Goal of T ; :: thesis: verum