theorem Th2: :: BAGORD_2:14

for a being object
for N being multLoopStr
for M being RelExtension of N holds
( a is Element of M iff a is Element of N )