let X be non empty TopSpace; :: thesis: {} X, [#] X constitute_a_decomposition
thus {} X, [#] X constitute_a_decomposition :: thesis: verum

proof

[#] X = ({} X) ` ;
hence {} X, [#] X constitute_a_decomposition by Th6; :: thesis: verum

end;