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

now :: thesis:

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

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

proof

let e be object ; :: 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, Th32; :: thesis:

end;

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

now :: thesis:

let e be object ; :: 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 :: thesis:

per cases ;

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

then e in B by A10, A13, XBOOLE_0:def 4;
then consider u being set such that
A14: ( e in u & u in P ) by A7, 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 and
A17: u in Q ; :: thesis:

now :: thesis:

per cases by A17, XBOOLE_0:def 3;

suppose u in P ; :: thesis:

then e in B by A7, A16, TARSKI:def 4;
hence e in C by A10, 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
A18: u = {x} and
A19: x in C \ ([#] Y) ;
e = x by A16, A18, TARSKI:def 1;
hence e in C by A19, XBOOLE_0:def 5; :: thesis:

end;

hence e in C ; :: thesis:

end;

then C = union Q by TARSKI:def 4;
hence Q in the topology of (space (TrivExt D)) by A2, A1, A9; :: thesis:
P c= Q by XBOOLE_1:7;
hence P c= Q /\ ([#] (space D)) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis:
let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A20: e in Q /\ ([#] (space D)) ; :: thesis:
then A21: e in [#] (space D) ;

A22: now :: 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
A23: e = {x} and
A24: x in C \ ([#] Y) ;
A25: not x in the carrier of Y by A24, XBOOLE_0:def 5;
then not (Proj (TrivExt D)) . x in the carrier of (space D) by Th36;
hence contradiction by A21, A23, A25, Th34; :: thesis:

end;

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

end;

given Q being Subset of (space (TrivExt D)) such that A26: Q in the topology of (space (TrivExt D)) and
A27: P = Q /\ ([#] (space D)) ; :: thesis:
A28: union P is Subset of Y by A4, EQREL_1:61;

now :: thesis:

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

proof

assume A29: e in (union Q) /\ ([#] Y) ; :: thesis:
then A30: (Proj (TrivExt D)) . e in the carrier of (space D) by Th37;
e in union Q by A29, XBOOLE_0:def 4;
then consider u being set such that
A31: e in u and
A32: u in Q by TARSKI:def 4;
take u ; :: thesis:
thus e in u by A31; :: thesis:
u is Element of TrivExt D by A32, Def7;
then u = (Proj (TrivExt D)) . e by A31, EQREL_1:65;
hence u in P by A27, A32, A30, XBOOLE_0:def 4; :: thesis:

end;

given u being set such that A33: e in u and
A34: u in P ; :: thesis:
u in Q by A27, A34, XBOOLE_0:def 4;
then A35: e in union Q by A33, TARSKI:def 4;
e in union P by A33, A34, TARSKI:def 4;
hence e in (union Q) /\ ([#] Y) by A28, A35, XBOOLE_0:def 4; :: thesis:

end;

then A36: union P = (union Q) /\ ([#] Y) by TARSKI:def 4;
ex A being Subset of (TrivExt D) st
( Q = A & union A in the topology of X ) by A1, A26;
then union P in the topology of Y by A36, PRE_TOPC:def 4;
hence P in the topology of (space D) by A4, A3; :: thesis:

end;

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

proof

let A be Subset of (space (TrivExt D)); :: according to BORSUK_1:def 11 :: thesis:
assume A37: A = the carrier of T ; :: thesis:
reconsider C = A ` as Subset of (TrivExt D) by Def7;
reconsider B = union A as Subset of X by A2, EQREL_1:61;
B = the carrier of Y by A4, A37, EQREL_1:def 4;
then B is closed by Def11;
then A38: B ` in the topology of X by PRE_TOPC:def 2;
union C = B ` by A2, EQREL_1:63;
then A ` in the topology of (space (TrivExt D)) by A38, Th27;
then A ` is open ;
hence A is closed by TOPS_1:3; :: thesis:

end;

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