let X be non trivial TopSpace; :: thesis: for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
let Y1 be non empty proper SubSpace of X; :: thesis: ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;
A1 is proper by TEX_2:8;
then consider Y2 being non empty strict SubSpace of X such that
A1: A1 ` = the carrier of Y2 by TSEP_1:10;
A2: for P, Q being Subset of X st P = the carrier of Y1 & Q = the carrier of Y2 holds
P,Q constitute_a_decomposition by A1, TSEP_2:5;
then Y1,Y2 constitute_a_decomposition ;
then reconsider Y2 = Y2 as non empty strict proper SubSpace of X by Th6;
take Y2 ; :: thesis: Y1,Y2 constitute_a_decomposition
thus Y1,Y2 constitute_a_decomposition by A2; :: thesis: verum