let T be non empty TopSpace; :: thesis: for S being non empty a_partition of the carrier of T
for A being Subset of ()
for B being Subset of T st B = union A holds
( A is closed iff B is closed )

let S be non empty a_partition of the carrier of T; :: thesis: for A being Subset of ()
for B being Subset of T st B = union A holds
( A is closed iff B is closed )

let A be Subset of (); :: thesis: for B being Subset of T st B = union A holds
( A is closed iff B is closed )

let B be Subset of T; :: thesis: ( B = union A implies ( A is closed iff B is closed ) )
reconsider C = A as Subset of S by BORSUK_1:def 7;
A1: ([#] T) \ () = () \ () by EQREL_1:def 4
.= union (S \ A) by EQREL_1:43
.= union (([#] ()) \ A) by BORSUK_1:def 7 ;
assume A2: B = union A ; :: thesis: ( A is closed iff B is closed )
thus ( A is closed implies B is closed ) :: thesis: ( B is closed implies A is closed )
proof
reconsider om = ([#] ()) \ A as Subset of S by BORSUK_1:def 7;
assume A is closed ; :: thesis: B is closed
then ([#] ()) \ A is open ;
then om in the topology of () ;
then ([#] T) \ B in the topology of T by ;
then ([#] T) \ B is open ;
hence B is closed ; :: thesis: verum
end;
thus ( B is closed implies A is closed ) :: thesis: verum
proof
reconsider om = ([#] ()) \ A as Subset of S by BORSUK_1:def 7;
assume B is closed ; :: thesis: A is closed
then ([#] T) \ B is open ;
then ([#] T) \ () in the topology of T by A2;
then om in the topology of () by ;
then ([#] ()) \ A is open ;
hence A is closed ; :: thesis: verum
end;