take ({} T) ` ; :: thesis: ({} T) ` is open
thus ({} T) ` is open ; :: thesis: verum