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

proof

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;

hence T_0-canonical_map T is open ; :: thesis: verum