take S ; :: thesis: ( not S is empty & S is S -headed )
thus ( not S is empty & S is S -headed ) by Th50; :: thesis: verum