theorem Th21: :: GCD_1:21

for R being non empty well-unital multLoopStr
for X being Subset of R st X in Classes R holds
not X is empty