Proving join-closure