consider J being MSSetOp of the Sorts of D such that
A1: for X being Element of bool the Sorts of D
for SF being non-empty MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) ) holds
J .. X = meet SF by Th33;
reconsider J = J as MSClosureOperator of the Sorts of D by A1, Th36, Th37;
take J ; :: thesis: for X being Element of bool the Sorts of D
for SF being non-empty MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) ) holds
J .. X = meet SF
thus for X being Element of bool the Sorts of D
for SF being non-empty MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) ) holds
J .. X = meet SF by A1; :: thesis: verum