set p = <% the Instruction of S%>;
take <% the Instruction of S%> ; :: thesis: ( <% the Instruction of S%> is initial & <% the Instruction of S%> is 1 -element & <% the Instruction of S%> is NAT -defined & <% the Instruction of S%> is the InstructionsF of S -valued )
thus ( <% the Instruction of S%> is initial & <% the Instruction of S%> is 1 -element & <% the Instruction of S%> is NAT -defined & <% the Instruction of S%> is the InstructionsF of S -valued ) ; :: thesis: verum