reconsider P = Kv as Subdivision of Kv by Th11;
take P ; :: thesis: not P is void
thus not P is void ; :: thesis: verum