set E = EqRel (R,I);
let x, y be Element of (R / I); GROUP_1:def 12 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
; verum