theorem Th27: :: AIMLOOP:30

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 phi . Y c= Y holds
( ( for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y ) )