set l = the Element of NAT ;
set I = the Instruction of S;
take the Element of NAT .--> the Instruction of S ; :: thesis: ( not the Element of NAT .--> the Instruction of S is empty & the Element of NAT .--> the Instruction of S is trivial & the Element of NAT .--> the Instruction of S is NAT -defined & the Element of NAT .--> the Instruction of S is the Instructions of S -valued )
thus ( not the Element of NAT .--> the Instruction of S is empty & the Element of NAT .--> the Instruction of S is trivial & the Element of NAT .--> the Instruction of S is NAT -defined & the Element of NAT .--> the Instruction of S is the Instructions of S -valued ) ; :: thesis: verum