let P be SubdivisionStr of Kr; :: thesis: not P is empty-membered
( not |.Kr.| is empty & |.Kr.| = |.P.| ) by Th7, Th10;
hence not P is empty-membered by Th7; :: thesis: verum