:: deftheorem defines algebraic CLOSURE3:def 4 :
for S being non empty 1-sorted
for IT being ClosureSystem of S holds
( IT is algebraic iff ClSys->ClOp IT is algebraic );