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