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