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 Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let X be non empty SubSpace of XX; :: thesis: for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let D be non empty a_partition of the carrier of X; :: thesis: for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X
let e be Point of XX; :: thesis: ( (Proj (TrivExt D)) . e in the carrier of (space D) implies e in the carrier of X )
assume (Proj (TrivExt D)) . e in the carrier of (space D) ; :: thesis: e in the carrier of X
then A1: (Proj (TrivExt D)) . e in D by Def7;
e in (Proj (TrivExt D)) . e by EQREL_1:def 9;
hence e in the carrier of X by A1; :: thesis: verum