let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is everywhere_dense iff B is nowhere_dense )
let A, B be Subset of X; :: thesis: ( A,B constitute_a_decomposition implies ( A is everywhere_dense iff B is nowhere_dense ) )
assume A1: A,B constitute_a_decomposition ; :: thesis: ( A is everywhere_dense iff B is nowhere_dense )
then B = A ` by TSEP_2:3;
hence ( A is everywhere_dense implies B is nowhere_dense ) by TOPS_3:39; :: thesis: ( B is nowhere_dense implies A is everywhere_dense )
assume A2: B is nowhere_dense ; :: thesis: A is everywhere_dense
A = B ` by A1, TSEP_2:3;
hence A is everywhere_dense by A2, TOPS_3:40; :: thesis: verum