let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )
let A, B be Subset of X; :: thesis: ( A,B constitute_a_decomposition implies ( not A is empty iff B is proper ) )
assume A1: A,B constitute_a_decomposition ; :: thesis: ( not A is empty iff B is proper )
then A2: B = A ` by TSEP_2:3;
thus ( not A is empty implies B is proper ) by A2, TOPS_3:1, SUBSET_1:def 6; :: thesis: ( B is proper implies not A is empty )
assume A3: B is proper ; :: thesis: not A is empty
A = B ` by A1, TSEP_2:3;
hence not A is empty by A3; :: thesis: verum