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