reconsider A = a, B = b as Data-Location by Th5;
reconsider i = A := B as Instruction of SCM+FSA by Th10;
take i ; :: thesis: ex A, B being Data-Location st
( a = A & b = B & i = A := B )
take A ; :: thesis: ex B being Data-Location st
( a = A & b = B & i = A := B )
take B ; :: thesis: ( a = A & b = B & i = A := B )
thus ( a = A & b = B & i = A := B ) ; :: thesis: verum