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;

T is closed

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: ( [#] (space D) c= [#] (space (TrivExt D)) & ( for P being Subset of (space D) holds

( ( 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)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) ) ) )

then reconsider T = space D as SubSpace of space (TrivExt D) by PRE_TOPC:def 4;( ( 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)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) ) ) )

thus
[#] (space D) c= [#] (space (TrivExt D))
by A5, XBOOLE_1:7; :: thesis: for P being Subset of (space D) holds

( ( 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)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )

let P be Subset of (space D); :: thesis: ( ( 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)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )

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: ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) )

A27: P = Q /\ ([#] (space D)) ; :: thesis: P in the topology of (space D)

A28: union P is Subset of Y by A4, EQREL_1:61;

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: verum

end;( ( 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)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )

let P be Subset of (space D); :: thesis: ( ( 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)) ) ) & ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) ) )

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: ( ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) ) implies P in the topology of (space D) )

proof

given Q being Subset of (space (TrivExt D)) such that A26:
Q in the topology of (space (TrivExt D))
and
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: ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )

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

take Q ; :: thesis: ( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )

hence Q in the topology of (space (TrivExt D)) by A2, A1, A9; :: thesis: P = Q /\ ([#] (space D))

P c= Q by XBOOLE_1:7;

hence P c= Q /\ ([#] (space D)) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: Q /\ ([#] (space D)) c= P

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Q /\ ([#] (space D)) or e in P )

assume A20: e in Q /\ ([#] (space D)) ; :: thesis: e in P

then A21: e in [#] (space D) ;

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

end;then A6: P c= TrivExt D by A4;

assume P in the topology of (space D) ; :: thesis: ex Q being Subset of (space (TrivExt D)) st

( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )

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

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;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { {x} where x is Point of X : x in C \ ([#] Y) } or e in TrivExt D )

assume e in { {x} where x is Point of X : x in C \ ([#] Y) } ; :: thesis: e in TrivExt D

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: verum

end;assume e in { {x} where x is Point of X : x in C \ ([#] Y) } ; :: thesis: e in TrivExt D

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: verum

take Q ; :: thesis: ( Q in the topology of (space (TrivExt D)) & P = Q /\ ([#] (space D)) )

now :: thesis: for e being object holds

( ( e in C implies ex u being set st

( e in u & u in Q ) ) & ( ex u being set st

( e in u & u in Q ) implies e in C ) )

then
C = union Q
by TARSKI:def 4;( ( e in C implies ex u being set st

( e in u & u in Q ) ) & ( ex u being set st

( e in u & u in Q ) implies e in C ) )

let e be object ; :: thesis: ( ( e in C implies ex u being set st

( e in u & u in Q ) ) & ( ex u being set st

( e in u & u in Q ) implies e in C ) )

thus ( e in C implies ex u being set st

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

( e in u & u in Q ) implies e in C )

A17: u in Q ; :: thesis: e in C

end;( e in u & u in Q ) ) & ( ex u being set st

( e in u & u in Q ) implies e in C ) )

thus ( e in C implies ex u being set st

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

( e in u & u in Q ) implies e in C )

proof

given u being set such that A16:
e in u
and
assume A13:
e in C
; :: thesis: ex u being set st

( e in u & u in Q )

then reconsider x = e as Point of X ;

( e in u & u in Q ) ; :: thesis: verum

end;( e in u & u in Q )

then reconsider x = e as Point of X ;

now :: thesis: ( ( e in [#] Y & ex u being set st

( e in u & u in Q ) ) or ( not e in [#] Y & ex u being set st

( e in u & u in Q ) ) )end;

hence
ex u being set st ( e in u & u in Q ) ) or ( not e in [#] Y & ex u being set st

( e in u & u in Q ) ) )

per cases
( e in [#] Y or not e in [#] Y )
;

end;

case
e in [#] Y
; :: thesis: ex u being set st

( e in u & u in Q )

( e in u & u in Q )

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: ( e in u & u in Q )

thus ( e in u & u in Q ) by A14, XBOOLE_0:def 3; :: thesis: verum

end;then consider u being set such that

A14: ( e in u & u in P ) by A7, TARSKI:def 4;

take u = u; :: thesis: ( e in u & u in Q )

thus ( e in u & u in Q ) by A14, XBOOLE_0:def 3; :: thesis: verum

case A15:
not e in [#] Y
; :: thesis: ex u being set st

( e in u & u in Q )

( e in u & u in Q )

take u = {e}; :: thesis: ( e in u & u in Q )

thus e in u by TARSKI:def 1; :: thesis: u in Q

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: verum

end;thus e in u by TARSKI:def 1; :: thesis: u in Q

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: verum

( e in u & u in Q ) ; :: thesis: verum

A17: u in Q ; :: thesis: e in C

now :: thesis: e in C

hence
e in C
; :: thesis: verumend;

hence Q in the topology of (space (TrivExt D)) by A2, A1, A9; :: thesis: P = Q /\ ([#] (space D))

P c= Q by XBOOLE_1:7;

hence P c= Q /\ ([#] (space D)) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: Q /\ ([#] (space D)) c= P

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Q /\ ([#] (space D)) or e in P )

assume A20: e in Q /\ ([#] (space D)) ; :: thesis: e in P

then A21: e in [#] (space D) ;

A22: now :: thesis: not e in { {x} where x is Point of X : x in C \ ([#] Y) }

e in Q
by A20, XBOOLE_0:def 4;assume
e in { {x} where x is Point of X : x in C \ ([#] Y) }
; :: thesis: contradiction

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: verum

end;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: verum

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

A27: P = Q /\ ([#] (space D)) ; :: thesis: P in the topology of (space D)

A28: union P is Subset of Y by A4, EQREL_1:61;

now :: thesis: for e being object holds

( ( e in (union Q) /\ ([#] Y) implies ex u being set st

( e in u & u in P ) ) & ( ex u being set st

( e in u & u in P ) implies e in (union Q) /\ ([#] Y) ) )

then A36:
union P = (union Q) /\ ([#] Y)
by TARSKI:def 4;( ( e in (union Q) /\ ([#] Y) implies ex u being set st

( e in u & u in P ) ) & ( ex u being set st

( e in u & u in P ) implies e in (union Q) /\ ([#] Y) ) )

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

( e in u & u in P ) ) & ( ex u being set st

( e in u & u in P ) implies e in (union Q) /\ ([#] Y) ) )

thus ( e in (union Q) /\ ([#] Y) implies ex u being set st

( e in u & u in P ) ) :: thesis: ( ex u being set st

( e in u & u in P ) implies e in (union Q) /\ ([#] Y) )

A34: u in P ; :: thesis: e in (union Q) /\ ([#] Y)

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: verum

end;( e in u & u in P ) ) & ( ex u being set st

( e in u & u in P ) implies e in (union Q) /\ ([#] Y) ) )

thus ( e in (union Q) /\ ([#] Y) implies ex u being set st

( e in u & u in P ) ) :: thesis: ( ex u being set st

( e in u & u in P ) implies e in (union Q) /\ ([#] Y) )

proof

given u being set such that A33:
e in u
and
assume A29:
e in (union Q) /\ ([#] Y)
; :: thesis: ex u being set st

( e in u & u in P )

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: ( e in u & u in P )

thus e in u by A31; :: thesis: u in P

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: verum

end;( e in u & u in P )

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: ( e in u & u in P )

thus e in u by A31; :: thesis: u in P

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: verum

A34: u in P ; :: thesis: e in (union Q) /\ ([#] Y)

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: verum

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: verum

T is closed

proof

hence
space D is strict closed SubSpace of space (TrivExt D)
; :: thesis: verum
let A be Subset of (space (TrivExt D)); :: according to BORSUK_1:def 11 :: thesis: ( A = the carrier of T implies A is closed )

assume A37: A = the carrier of T ; :: thesis: A is closed

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: verum

end;assume A37: A = the carrier of T ; :: thesis: A is closed

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: verum