Claim:
Pf: essentially same as (close/open the loop, apply the relations to prove 'open' is well defined)