consider l being Element of NAT , I being Instruction of S;
take l .--> I ; :: thesis: ( not l .--> I is empty & l .--> I is trivial & l .--> I is NAT -defined & l .--> I is the Instructions of S -valued )
thus ( not l .--> I is empty & l .--> I is trivial & l .--> I is NAT -defined & l .--> I is the Instructions of S -valued ) ; :: thesis: verum