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