A1: the carrier of (space D) = D by Def10;
A2: the topology of (space D) = { A where A is Subset of D : union A in the topology of Y } by Def10;
A3: the carrier of (space (TrivExt D)) = TrivExt D by Def10;
A4: the topology of (space (TrivExt D)) = { A where A is Subset of (TrivExt D) : union A in the topology of X } by Def10;
A5: ( [#] (space D) = D & [#] (space (TrivExt D)) = TrivExt D ) by Def10;

now

thus [#] (space D) c= [#] (space (TrivExt D)) by A5, XBOOLE_1:7; :: thesis:
let P be Subset of (space D); :: thesis:
thus ( P in the topology of (space D) implies ex Q being Subset of (space (TrivExt D)) st
( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) ) :: thesis:

proof

assume P in the topology of (space D) ; :: thesis:
then consider A being Subset of D such that
A6: P = A and
A7: union A in the topology of Y by A2;
reconsider B = union A as Subset of Y by A7;
consider C being Subset of X such that
A8: C in the topology of X and
A9: B = C /\ ([#] Y) by A7, PRE_TOPC:def 9;
D c= TrivExt D by XBOOLE_1:7;
then A10: P c= TrivExt D by A1, XBOOLE_1:1;
{ {x} where x is Point of X : x in C \ ([#] Y) } c= TrivExt D

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in { {x} where x is Point of X : x in C \ ([#] Y) } ; :: thesis:
then consider x being Point of X such that
A11: e = {x} and
A12: x in C \ ([#] Y) ;
not x in the carrier of Y by A12, XBOOLE_0:def 5;
hence e in TrivExt D by A11, Th75; :: thesis:

end;

then reconsider Q = P \/ { {x} where x is Point of X : x in C \ ([#] Y) } as Subset of (space (TrivExt D)) by A3, A10, XBOOLE_1:8;

now

let e be set ; :: thesis:
thus ( e in C implies ex u being set st
( e in u & u in Q ) ) :: thesis:

proof

assume A13: e in C ; :: thesis:
then reconsider x = e as Point of X ;

now

per cases ;

case e in [#] Y ; :: thesis:

then e in B by A9, A13, XBOOLE_0:def 4;
then consider u being set such that
A14: ( e in u & u in P ) by A6, TARSKI:def 4;
take u = u; :: thesis:
thus ( e in u & u in Q ) by A14, XBOOLE_0:def 3; :: thesis:

end;

case A15: not e in [#] Y ; :: thesis:

take u = {e}; :: thesis:
thus e in u by TARSKI:def 1; :: thesis:
x in C \ ([#] Y) by A13, A15, XBOOLE_0:def 5;
then u in { {y} where y is Point of X : y in C \ ([#] Y) } ;
hence u in Q by XBOOLE_0:def 3; :: thesis:

end;

hence ex u being set st
( e in u & u in Q ) ; :: thesis:

end;

given u being set such that A16: ( e in u & u in Q ) ; :: thesis:

now

per cases by A16, XBOOLE_0:def 3;

suppose u in P ; :: thesis:

then e in B by A6, A16, TARSKI:def 4;
hence e in C by A9, XBOOLE_0:def 4; :: thesis:

end;

suppose u in { {x} where x is Point of X : x in C \ ([#] Y) } ; :: thesis:

then consider x being Point of X such that
A17: u = {x} and
A18: x in C \ ([#] Y) ;
e = x by A16, A17, TARSKI:def 1;
hence e in C by A18, XBOOLE_0:def 5; :: thesis:

end;

hence e in C ; :: thesis:

end;

then A19: C = union Q by TARSKI:def 4;
take Q ; :: thesis:
thus Q in the topology of (space (TrivExt D)) by A3, A4, A8, A19; :: thesis:
( P c= Q & P c= [#] (space D) ) by XBOOLE_1:7;
hence P c= Q /\ ([#] (space D)) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis:
let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in Q /\ ([#] (space D)) ; :: thesis:
then A20: ( e in Q & e in [#] (space D) ) by XBOOLE_0:def 4;

now

assume e in { {x} where x is Point of X : x in C \ ([#] Y) } ; :: thesis:
then consider x being Point of X such that
A21: e = {x} and
A22: x in C \ ([#] Y) ;
A23: not x in the carrier of Y by A22, XBOOLE_0:def 5;
then not (Proj (TrivExt D)) . x in the carrier of (space D) by Th79;
hence contradiction by A20, A21, A23, Th77; :: thesis:

end;

hence e in P by A20, XBOOLE_0:def 3; :: thesis:

end;

given Q being Subset of (space (TrivExt D)) such that A24: Q in the topology of (space (TrivExt D)) and
A25: P = Q /\ ([#] (space D)) ; :: thesis:
A26: ex A being Subset of (TrivExt D) st
( Q = A & union A in the topology of X ) by A4, A24;
A27: ( union Q is Subset of X & union P is Subset of Y ) by A1, A3, Th25;

now

let e be set ; :: thesis:
thus ( e in (union Q) /\ ([#] Y) implies ex u being set st
( e in u & u in P ) ) :: thesis:

proof

assume A28: e in (union Q) /\ ([#] Y) ; :: thesis:
then ( e in union Q & e in [#] Y ) by XBOOLE_0:def 4;
then consider u being set such that
A29: ( e in u & u in Q ) by TARSKI:def 4;
take u ; :: thesis:
thus e in u by A29; :: thesis:
A30: (Proj (TrivExt D)) . e in the carrier of (space D) by A28, Th80;
u is Element of TrivExt D by A29, Def10;
then u = (Proj (TrivExt D)) . e by A29, Th29;
hence u in P by A25, A29, A30, XBOOLE_0:def 4; :: thesis:

end;

given u being set such that A31: ( e in u & u in P ) ; :: thesis:
u in Q by A25, A31, XBOOLE_0:def 4;
then A32: e in union Q by A31, TARSKI:def 4;
e in union P by A31, TARSKI:def 4;
hence e in (union Q) /\ ([#] Y) by A27, A32, XBOOLE_0:def 4; :: thesis:

end;

then union P = (union Q) /\ ([#] Y) by TARSKI:def 4;
then union P in the topology of Y by A26, PRE_TOPC:def 9;
hence P in the topology of (space D) by A1, A2; :: thesis:

end;

then reconsider T = space D as SubSpace of space (TrivExt D) by PRE_TOPC:def 9;
T is closed

proof

let A be Subset of (space (TrivExt D)); :: according to BORSUK_1:def 14 :: thesis:
assume A33: A = the carrier of T ; :: thesis:
reconsider B = union A as Subset of X by A3, Th25;
reconsider C = A ` as Subset of (TrivExt D) by Def10;
A34: union C = B ` by A3, Th27;
B = the carrier of Y by A1, A33, EQREL_1:def 6;
then B is closed by Def14;
then B ` in the topology of X by PRE_TOPC:def 5;
then A ` in the topology of (space (TrivExt D)) by A34, Th69;
then A ` is open by PRE_TOPC:def 5;
hence A is closed by TOPS_1:29; :: thesis:

end;

hence space D is strict closed SubSpace of space (TrivExt D) ; :: thesis: