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

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 5;
hence union V in the topology of T by A1, BORSUK_1:69; :: 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:69;
hence V is open by PRE_TOPC:def 5; :: thesis: verum