let T be TopGroup; :: thesis: ( T is BinContinuous implies T is homogeneous )
assume T is BinContinuous ; :: thesis: T is homogeneous
then reconsider G = T as BinContinuous TopGroup ;
G is homogeneous

proof

let p, q be Point of G; :: according to TOPGRP_1:def 6 :: thesis: ex f being Homeomorphism of G st f . p = q
take * ((p " ) * q) ; :: thesis: (* ((p " ) * q)) . p = q
thus (* ((p " ) * q)) . p = p * ((p " ) * q) by Def2
.= (p * (p " )) * q by GROUP_1:def 4
.= (1_ G) * q by GROUP_1:def 6
.= q by GROUP_1:def 5 ; :: thesis: verum

end;

hence T is homogeneous ; :: thesis: verum