let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds X0,X0 do_not_constitute_a_decomposition
let X0 be non empty SubSpace of X; :: thesis: X0,X0 do_not_constitute_a_decomposition
reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;

now :: thesis: ex A1, A2 being Subset of X st
( A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2 do_not_constitute_a_decomposition )

take A1 = A0; :: thesis: ex A2 being Subset of X st
( A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2 do_not_constitute_a_decomposition )
take A2 = A0; :: thesis: ( A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2 do_not_constitute_a_decomposition )
thus ( A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2 do_not_constitute_a_decomposition ) by Th7; :: thesis: verum

end;

hence X0,X0 do_not_constitute_a_decomposition ; :: thesis: verum