let T be non empty TopSpace; :: thesis: for S being non empty a_partition of the carrier of T

for A being Subset of (space S)

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 (space S)

for B being Subset of T st B = union A holds

( A is closed iff B is closed )

let A be Subset of (space S); :: 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) \ (union A) = (union S) \ (union C) by EQREL_1:def 4

.= union (S \ A) by EQREL_1:43

.= union (([#] (space S)) \ 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 )

for A being Subset of (space S)

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 (space S)

for B being Subset of T st B = union A holds

( A is closed iff B is closed )

let A be Subset of (space S); :: 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) \ (union A) = (union S) \ (union C) by EQREL_1:def 4

.= union (S \ A) by EQREL_1:43

.= union (([#] (space S)) \ 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

thus
( B is closed implies A is closed )
:: thesis: verum
reconsider om = ([#] (space S)) \ A as Subset of S by BORSUK_1:def 7;

assume A is closed ; :: thesis: B is closed

then ([#] (space S)) \ A is open ;

then om in the topology of (space S) ;

then ([#] T) \ B in the topology of T by A2, A1, BORSUK_1:27;

then ([#] T) \ B is open ;

hence B is closed ; :: thesis: verum

end;assume A is closed ; :: thesis: B is closed

then ([#] (space S)) \ A is open ;

then om in the topology of (space S) ;

then ([#] T) \ B in the topology of T by A2, A1, BORSUK_1:27;

then ([#] T) \ B is open ;

hence B is closed ; :: thesis: verum

proof

reconsider om = ([#] (space S)) \ 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) \ (union A) in the topology of T by A2;

then om in the topology of (space S) by A1, BORSUK_1:27;

then ([#] (space S)) \ A is open ;

hence A is closed ; :: thesis: verum

end;assume B is closed ; :: thesis: A is closed

then ([#] T) \ B is open ;

then ([#] T) \ (union A) in the topology of T by A2;

then om in the topology of (space S) by A1, BORSUK_1:27;

then ([#] (space S)) \ A is open ;

hence A is closed ; :: thesis: verum