set i = the Instruction of S;
take (il. (S,0)) .--> the Instruction of S ; :: thesis: ( (il. (S,0)) .--> the Instruction of S is lower & (il. (S,0)) .--> the Instruction of S is 1 -element )
thus ( (il. (S,0)) .--> the Instruction of S is lower & (il. (S,0)) .--> the Instruction of S is 1 -element ) by Th25; :: thesis: verum