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