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

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