let l be Instruction-Location of IT; :: thesis: l is Element of
( l in NAT & NAT c= the carrier of IT ) by Def3, ORDINAL1:def 13;
hence l is Element of ; :: thesis: verum