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 )
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 ) by Th48; :: thesis: verum