theorem Th3: :: BAGORD_2:15

for N being multLoopStr
for M being RelExtension of N holds 1. N = 1. M