reconsider SS = S null as Language ;
take SS ; :: thesis: SS is S -extending
thus SS is S -extending ; :: thesis: verum