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