theorem Th34: :: AIMLOOP:37

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
( Mlt H is_a_fixpoint_of phi & ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Mlt H c= S ) )