let X be non empty TopSpace; :: thesis: for D being non empty a_partition of the carrier of X

for A being Subset of D holds

( union A in the topology of X iff A in the topology of (space D) )

let D be non empty a_partition of the carrier of X; :: thesis: for A being Subset of D holds

( union A in the topology of X iff A in the topology of (space D) )

let B be Subset of D; :: thesis: ( union B in the topology of X iff B in the topology of (space D) )

A1: the topology of (space D) = { A where A is Subset of D : union A in the topology of X } by Def7;

hence ( union B in the topology of X implies B in the topology of (space D) ) ; :: thesis: ( B in the topology of (space D) implies union B in the topology of X )

assume B in the topology of (space D) ; :: thesis: union B in the topology of X

then ex A being Subset of D st

( B = A & union A in the topology of X ) by A1;

hence union B in the topology of X ; :: thesis: verum

for A being Subset of D holds

( union A in the topology of X iff A in the topology of (space D) )

let D be non empty a_partition of the carrier of X; :: thesis: for A being Subset of D holds

( union A in the topology of X iff A in the topology of (space D) )

let B be Subset of D; :: thesis: ( union B in the topology of X iff B in the topology of (space D) )

A1: the topology of (space D) = { A where A is Subset of D : union A in the topology of X } by Def7;

hence ( union B in the topology of X implies B in the topology of (space D) ) ; :: thesis: ( B in the topology of (space D) implies union B in the topology of X )

assume B in the topology of (space D) ; :: thesis: union B in the topology of X

then ex A being Subset of D st

( B = A & union A in the topology of X ) by A1;

hence union B in the topology of X ; :: thesis: verum