set E = EqRel (R,I);

let x, y be Element of (R / I); :: according to GROUP_1:def 12 :: 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

let x, y be Element of (R / I); :: according to GROUP_1:def 12 :: 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