let X be non empty TopSpace; :: thesis: for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )
let Y1, Y2 be non empty SubSpace of X; :: thesis: ( Y1,Y2 constitute_a_decomposition implies ( Y1 is proper & Y2 is proper ) )
reconsider A1 = the carrier of Y1, A2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume Y1,Y2 constitute_a_decomposition ; :: thesis: ( Y1 is proper & Y2 is proper )
then A1,A2 constitute_a_decomposition ;
then ( A1 is proper & A2 is proper ) by Th1;
hence ( Y1 is proper & Y2 is proper ) by TEX_2:8; :: thesis: verum