consider l being Instruction-Location of S;
take a = <*l*>; :: thesis: not a is empty
thus not a is empty ; :: thesis: verum