let I be set ; :: thesis:
let M be ManySortedSet of I; :: thesis:
let D be properly-upper-bound MSSubsetFamily of M; :: thesis:
let J be MSSetOp of M; :: thesis:
assume A1: for X being Element of bool M
for SF being V8() MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ; :: thesis:
thus J is reflexive :: thesis:

let X be Element of bool M; :: according to CLOSURE1:def 1 :: thesis:
consider SF being V8() MSSubsetFamily of M such that
A2: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
( J .. X = meet SF & ( for Z1 being ManySortedSet of I st Z1 in SF holds
X c= Z1 ) ) by A1, A2;
hence X c= J .. X by MSSUBFAM:45; :: thesis:

end;

let x, y be Element of bool M; :: according to CLOSURE1:def 2 :: thesis:
assume A3: x c= y ; :: thesis:
consider SFx being V8() MSSubsetFamily of M such that
A4: for Y being ManySortedSet of I holds
( Y in SFx iff ( Y in D & x c= Y ) ) by Th31;
consider SFy being V8() MSSubsetFamily of M such that
A5: for Y being ManySortedSet of I holds
( Y in SFy iff ( Y in D & y c= Y ) ) by Th31;
SFy c= SFx

let i be object ; :: according to PBOOLE:def 2 :: thesis:
assume A6: i in I ; :: thesis:
then consider Fi being non empty set such that
A7: Fi = D . i ;
A8: x . i c= y . i by A3, A6;
( SFx . i = { t where t is Element of Fi : x . i c= t } & SFy . i = { z where z is Element of Fi : y . i c= z } ) by A4, A5, A6, A7, Th32;
hence SFy . i c= SFx . i by A8, Th1; :: thesis:

end;

end;