let X, Y be non empty TopSpace; :: thesis: for d being Function of X,Y holds
( d is relatively_open iff corestr d is open )
let d be Function of X,Y; :: thesis: ( d is relatively_open iff corestr d is open )
A1: corestr d = d by WAYBEL18:def 7;
A2: Image d = Y | (rng d) by WAYBEL18:def 6;
thus ( d is relatively_open implies corestr d is open ) by A1, A2; :: thesis: ( corestr d is open implies d is relatively_open )
assume A3: for V being Subset of X st V is open holds
(corestr d) .: V is open ; :: according to T_0TOPSP:def 2 :: thesis: d is relatively_open
let V be open Subset of X; :: according to WAYBEL34:def 9 :: thesis: d .: V is open Subset of (Y | (rng d))
thus d .: V is open Subset of (Y | (rng d)) by A1, A2, A3; :: thesis: verum