:: deftheorem Def22 defines Cl CLOSURE2:def 22 :
for S being 1-sorted
for A being ClosureSystem of S
for C being ManySortedSubset of the Sorts of A
for b₄ being Element of Bool the Sorts of A holds
( b₄ = Cl C iff ex F being SubsetFamily of the Sorts of A st
( b₄ = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) );