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