let X be non empty TopSpace; :: thesis: {} X, [#] X constitute_a_decomposition
[#] X = ({} X) ` ;
hence {} X, [#] X constitute_a_decomposition by Th6; :: thesis: verum