take {X} ; :: thesis: ( {X} is Subset-Family of X & {X} is a_partition of X & not {X} is empty )
thus ( {X} is Subset-Family of X & {X} is a_partition of X & not {X} is empty ) by Th39; :: thesis: verum