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

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