theorem Th28: :: AIMLOOP:31

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 ( for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
Y c= S ) holds
for f being Element of Funcs (Q,Q) st f in Y holds
f is Permutation of Q