let p be FinPartState of ; :: thesis: for k being Element of NAT holds Start-At ((IC p) + k) c= Relocated p,k
let k be Element of NAT ; :: thesis: Start-At ((IC p) + k) c= Relocated p,k
A1: IC (Relocated p,k) = (IC p) + k by Th26;
A2: IC SCM in dom (Relocated p,k) by Th25;
then IC (Relocated p,k) = (Relocated p,k) . (IC SCM ) by AMI_1:def 43;
then A3: ( Start-At ((IC p) + k) = {[(IC SCM ),((IC p) + k)]} & [(IC SCM ),((IC p) + k)] in Relocated p,k ) by A2, A1, FUNCT_1:def 4, FUNCT_4:87;
thus Start-At ((IC p) + k) c= Relocated p,k :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Start-At ((IC p) + k) or x in Relocated p,k )
assume x in Start-At ((IC p) + k) ; :: thesis: x in Relocated p,k
hence x in Relocated p,k by A3, TARSKI:def 1; :: thesis: verum

end;