theorem Th29: :: AIMLOOP:32

for Q being multLoop
for H being Subset of Q
for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds
for Y being Subset of (Funcs (Q,Q)) st Y is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
( Y is composition-closed & Y is inverse-closed )