let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is dense iff B is boundary )
let A, B be Subset of X; :: thesis: ( A,B constitute_a_decomposition implies ( A is dense iff B is boundary ) )
assume A1: A,B constitute_a_decomposition ; :: thesis: ( A is dense iff B is boundary )
then B = A ` by TSEP_2:3;
hence ( A is dense implies B is boundary ) by TOPS_3:18; :: thesis: ( B is boundary implies A is dense )
assume A2: B is boundary ; :: thesis: A is dense
A = B ` by A1, TSEP_2:3;
hence A is dense by A2, TOPS_1:def 4; :: thesis: verum