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 3
.= (1_ G) * q by GROUP_1:def 5
.= q by GROUP_1:def 4 ; :: thesis: verum

end;

hence T is homogeneous ; :: thesis: verum