let T be non empty TopSpace; :: thesis: for V being Subset of (T_0-reflex T) holds
( V is open iff union V in the topology of T )
let V be Subset of (T_0-reflex T); :: thesis: ( V is open iff union V in the topology of T )
A1: V is Subset of (Indiscernible T) by BORSUK_1:def 7;

hereby :: thesis: ( union V in the topology of T implies V is open )

assume V is open ; :: thesis: union V in the topology of T
then V in the topology of (T_0-reflex T) by PRE_TOPC:def 2;
hence union V in the topology of T by A1, BORSUK_1:27; :: thesis: verum

end;

assume union V in the topology of T ; :: thesis: V is open
then V in the topology of (space (Indiscernible T)) by A1, BORSUK_1:27;
hence V is open by PRE_TOPC:def 2; :: thesis: verum