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 & Image d = Y | (rng d) ) by WAYBEL18:def 6, WAYBEL18:def 7;
thus ( d is relatively_open implies corestr d is open ) :: thesis: ( corestr d is open implies d is relatively_open )

proof

assume A2: for V being open Subset of X holds d .: V is open Subset of (Y | (rng d)) ; :: according to WAYBEL34:def 9 :: thesis: corestr d is open
let V be Subset of X; :: according to T_0TOPSP:def 2 :: thesis: ( not V is open or (corestr d) .: V is open )
assume V is open ; :: thesis: (corestr d) .: V is open
hence (corestr d) .: V is open by A1, A2; :: thesis: verum

end;

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