consider I being Instruction of S;
consider l being Element of NAT ;
take l .--> I ; :: thesis: ( not l .--> I is empty & l .--> I is trivial & l .--> I is autonomic & l .--> I is NAT -defined )
thus ( not l .--> I is empty & l .--> I is trivial & l .--> I is autonomic & l .--> I is NAT -defined ) by Lm1; :: thesis: verum