let f be Function of S,T; :: thesis: ( f is being_homeomorphism implies f is open )
assume A1: f is being_homeomorphism ; :: thesis: f is open
let A be Subset of S; :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or f .: A is open )
thus ( not A is open or f .: A is open ) by A1, Th25; :: thesis: verum