reconsider p = <%> the InstructionsF of S as preProgram of S ;
take p ; :: thesis: p is empty
thus p is empty ; :: thesis: verum