:: deftheorem Def3 defines |: CLOSURE2:def 3 :
for I being set
for M being ManySortedSet of I
for S being SubsetFamily of M holds
( ( S <> {} implies |:S:| = |.S.| ) & ( not S <> {} implies |:S:| = EmptyMS I ) );