let XX be non empty TopSpace; :: thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let X be non empty SubSpace of XX; :: thesis: for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let D be non empty a_partition of the carrier of X; :: thesis: for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)
let e be set ; :: thesis: ( e in the carrier of X implies (Proj (TrivExt D)) . e in the carrier of (space D) )
assume A1: e in the carrier of X ; :: thesis: (Proj (TrivExt D)) . e in the carrier of (space D)
then reconsider x = e as Point of X ;
the carrier of X c= the carrier of XX by Th1;
then (Proj D) . x = (Proj (TrivExt D)) . x by A1, Th33;
hence (Proj (TrivExt D)) . e in the carrier of (space D) ; :: thesis: verum