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;

thus ( V is open implies union V in the topology of T ) by A1, BORSUK_1:27; :: thesis: ( union V in the topology of T implies V is open )

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

( 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;

thus ( V is open implies union V in the topology of T ) by A1, BORSUK_1:27; :: thesis: ( union V in the topology of T implies V is open )

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