take {} GX ; :: thesis: {} GX is boundary
thus {} GX is boundary ; :: thesis: verum