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

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