let T be non empty TopSpace; :: thesis: for A being non empty a_partition of the carrier of T
for y being Subset of (space A) holds (Proj A) " y = union y
let A be non empty a_partition of the carrier of T; :: thesis: for y being Subset of (space A) holds (Proj A) " y = union y
let y be Subset of (space A); :: thesis: (Proj A) " y = union y
reconsider y = y as Subset of A by BORSUK_1:def 7;
(Proj A) " y = (proj A) " y by BORSUK_1:def 8
.= union y by EQREL_1:67 ;
hence (Proj A) " y = union y ; :: thesis: verum