let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 is open iff A2 is closed )
let A1, A2 be Subset of X; :: thesis: ( A1,A2 constitute_a_decomposition implies ( A1 is open iff A2 is closed ) )
assume A1: A1,A2 constitute_a_decomposition ; :: thesis: ( A1 is open iff A2 is closed )
then A2 = A1 ` by Th3;
hence ( A1 is open implies A2 is closed ) by TOPS_1:4; :: thesis: ( A2 is closed implies A1 is open )
assume A2: A2 is closed ; :: thesis: A1 is open
A1 = A2 ` by A1, Th3;
hence A1 is open by A2, TOPS_1:3; :: thesis: verum