theorem Th13: :: HILBASIS:13

for X being set
for x being Element of X
for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)}