:: deftheorem Def5 defines HomeoGroup TOPGRP_1:def 5 :
for T being TopStruct
for b₂ being strict multMagma holds
( b₂ = HomeoGroup T iff for x being set holds
( ( x in the carrier of b₂ implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b₂ ) & ( for f, g being Homeomorphism of T holds the multF of b₂ . (f,g) = g * f ) ) );