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

( 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