theorem Th4: :: MIDSP_1:4

for a, b, c, d being Element of Example holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )