reconsider A = a, B = b as Data-Location by Th25;
reconsider i = A := B as Instruction of SCM+FSA by Th38;
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