theorem :: GROUP_24:93

for g1 being Element of INT.Group
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group +infty) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ INT.Group),a2*> holds
y * x = (x ") * y