:: deftheorem defines algebraic CLOSURE3:def 3 :
for I being non empty set
for M being ManySortedSet of I
for S being SetOp of M holds
( S is algebraic iff for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A = { (S . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A ) );