let a, b be Int-Location; :: thesis: InsCode (SubFrom (a,b)) = 3
ex A, B being Data-Location st
( a = A & b = B & SubFrom (a,b) = SubFrom (A,B) ) by Def8;
hence InsCode (SubFrom (a,b)) = 3 ; :: thesis: verum