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;

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 )

hence
X0,X0 do_not_constitute_a_decomposition
; :: thesis: verum( 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;( 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