set M = the Sorts of D;
let Q1, Q2 be MSClosureOperator of the Sorts of D; :: thesis: ( ( for X being Element of bool the Sorts of D
for SF being V8() 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
Q1 .. X = meet SF ) & ( for X being Element of bool the Sorts of D
for SF being V8() 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
Q2 .. X = meet SF ) implies Q1 = Q2 )
assume that
A2: for X being Element of bool the Sorts of D
for SF being V8() 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
Q1 .. X = meet SF and
A3: for X being Element of bool the Sorts of D
for SF being V8() 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
Q2 .. X = meet SF ; :: thesis: Q1 = Q2
now :: thesis: for x being ManySortedSet of the carrier of S st x in bool the Sorts of D holds
Q1 .. x = Q2 .. x
let x be ManySortedSet of the carrier of S; :: thesis: ( x in bool the Sorts of D implies Q1 .. x = Q2 .. x )
assume x in bool the Sorts of D ; :: thesis: Q1 .. x = Q2 .. x
then A4: x is Element of bool the Sorts of D by MSSUBFAM:11;
then consider SF being V8() MSSubsetFamily of the Sorts of D such that
A5: for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & x c= Y ) ) by Th31;
thus Q1 .. x = meet SF by A2, A4, A5
.= Q2 .. x by A3, A4, A5 ; :: thesis: verum
end;
hence Q1 = Q2 by Th7; :: thesis: verum