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