set i = the Instruction of S;
take (il. (S,0)) .--> the Instruction of S ; :: thesis: ( (il. (S,0)) .--> the Instruction of S is lower & not (il. (S,0)) .--> the Instruction of S is empty & (il. (S,0)) .--> the Instruction of S is trivial & (il. (S,0)) .--> the Instruction of S is NAT -defined & (il. (S,0)) .--> the Instruction of S is the Instructions of S -valued )
thus ( (il. (S,0)) .--> the Instruction of S is lower & not (il. (S,0)) .--> the Instruction of S is empty & (il. (S,0)) .--> the Instruction of S is trivial & (il. (S,0)) .--> the Instruction of S is NAT -defined & (il. (S,0)) .--> the Instruction of S is the Instructions of S -valued ) by Th48; :: thesis: verum