let T be non empty TopSpace; :: thesis: T_0-canonical_map T is open

set F = T_0-canonical_map T;

for A being Subset of T st A is open holds

(T_0-canonical_map T) .: A is open

set F = T_0-canonical_map T;

for A being Subset of T st A is open holds

(T_0-canonical_map T) .: A is open

proof

hence
T_0-canonical_map T is open
; :: thesis: verum
set D = Indiscernible T;

A1: T_0-canonical_map T = proj (Indiscernible T) by BORSUK_1:def 8;

let A be Subset of T; :: thesis: ( A is open implies (T_0-canonical_map T) .: A is open )

assume A2: A is open ; :: thesis: (T_0-canonical_map T) .: A is open

A3: for C being Subset of T st C in Indiscernible T & C meets A holds

C c= A by A2, Th7;

set A9 = (T_0-canonical_map T) .: A;

(T_0-canonical_map T) .: A is Subset of (Indiscernible T) by BORSUK_1:def 7;

then (T_0-canonical_map T) " ((T_0-canonical_map T) .: A) = union ((T_0-canonical_map T) .: A) by A1, EQREL_1:67;

then A = union ((T_0-canonical_map T) .: A) by A1, A3, EQREL_1:69;

then union ((T_0-canonical_map T) .: A) in the topology of T by A2;

hence (T_0-canonical_map T) .: A is open by Th2; :: thesis: verum

end;A1: T_0-canonical_map T = proj (Indiscernible T) by BORSUK_1:def 8;

let A be Subset of T; :: thesis: ( A is open implies (T_0-canonical_map T) .: A is open )

assume A2: A is open ; :: thesis: (T_0-canonical_map T) .: A is open

A3: for C being Subset of T st C in Indiscernible T & C meets A holds

C c= A by A2, Th7;

set A9 = (T_0-canonical_map T) .: A;

(T_0-canonical_map T) .: A is Subset of (Indiscernible T) by BORSUK_1:def 7;

then (T_0-canonical_map T) " ((T_0-canonical_map T) .: A) = union ((T_0-canonical_map T) .: A) by A1, EQREL_1:67;

then A = union ((T_0-canonical_map T) .: A) by A1, A3, EQREL_1:69;

then union ((T_0-canonical_map T) .: A) in the topology of T by A2;

hence (T_0-canonical_map T) .: A is open by Th2; :: thesis: verum