set E = EqRel R,I;
let x, y be Element of (R / I); :: according to GROUP_1:def 16 :: thesis: x * y = y * x
consider a being Element of R such that
A1: x = Class (EqRel R,I),a by Th11;
consider b being Element of R such that
A2: y = Class (EqRel R,I),b by Th11;
thus x * y = Class (EqRel R,I),(a * b) by A1, A2, Th14
.= y * x by A1, A2, Th14 ; :: thesis: verum