let T be TopStruct ; :: thesis: for f being Homeomorphism of T holds f /" is Homeomorphism of T
let f be Homeomorphism of T; :: thesis: f /" is Homeomorphism of T
thus f /" is being_homeomorphism ; :: according to TOPGRP_1:def 4 :: thesis: verum