theorem :: TOPGRP_1:61

for T being TopStruct
for f being Function of T,T st T is empty holds
f is being_homeomorphism by Lm2;