let I be set ; :: thesis:
let M be ManySortedSet of I; :: thesis:
let D be properly-upper-bound MSSubsetFamily of M; :: thesis:
set G = bool M;
defpred S₁[ object , object , object ] means ex D2 being set st
( D2 = $2 & ( for sf being Subset-Family of (M . $3)
for Fi being non empty set st Fi = D . $3 & sf = { z where z is Element of Fi : D2 c= z } holds
$1 = Intersect sf ) );

consider K being ManySortedSet of I such that
A2: K in bool M by PBOOLE:134;
let i be object ; :: thesis:
assume A3: i in I ; :: thesis:
reconsider b = (bool M) . i as non empty set by A3;
let x be object ; :: thesis:
assume A4: x in (bool M) . i ; :: thesis:
dom (K +* (i .--> x)) = I by A3, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A5: dom (i .--> x) = {i} ;
i in {i} by TARSKI:def 1;
then A6: X . i = (i .--> x) . i by A5, FUNCT_4:13
.= x by FUNCOP_1:72 ;
A7: X is Element of bool M

let s be object ; :: according to PBOOLE:def 14 :: thesis:
assume A8: s in I ; :: thesis:

hence X . s is Element of (bool M) . s by A4, A6; :: thesis:

end;

end;

then consider SF being non-empty MSSubsetFamily of M such that
A9: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
reconsider sf = SF . i as Subset-Family of (M . i) by A3, MSSUBFAM:32;
reconsider q = Intersect sf as Element of b by A3, MBOOLEAN:def 1;
reconsider s = b --> q as Function of b,b ;
reconsider y = s . x as object ;
take y = y; :: thesis:
Intersect sf in bool (M . i) ;
then Intersect sf in b by A3, MBOOLEAN:def 1;
hence y in (bool M) . i by A4, FUNCOP_1:7; :: thesis:
thus S₁[y,x,i] :: thesis:

reconsider Di = D . i as non empty set by A3;
A10: SF . i = { z where z is Element of Di : X . i c= z } by A3, A7, A9, Th32;
reconsider xx = x as set by TARSKI:1;
take xx ; :: thesis:
thus xx = x ; :: thesis:
let sf1 be Subset-Family of (M . i); :: thesis:
let Fi be non empty set ; :: thesis:
assume ( Fi = D . i & sf1 = { z where z is Element of Fi : xx c= z } ) ; :: thesis:
hence y = Intersect sf1 by A4, A6, A10, FUNCOP_1:7; :: thesis:

end;

consider J being ManySortedFunction of bool M, bool M such that
A11: for i being object st i in I holds
ex f being Function of ((bool M) . i),((bool M) . i) st
( f = J . i & ( for x being object st x in (bool M) . i holds
S₁[f . x,x,i] ) ) from MSSUBFAM:sch 1(A1);
reconsider J = J as MSSetOp of M ;
take J ; :: thesis:
let X be Element of bool M; :: thesis:
let SF be non-empty MSSubsetFamily of M; :: thesis:
assume A12: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ; :: thesis:

let i be object ; :: thesis:
assume A13: i in I ; :: thesis:
then consider Q being Subset-Family of (M . i) such that
A14: Q = SF . i and
A15: (meet SF) . i = Intersect Q by MSSUBFAM:def 1;
reconsider Fi = D . i as non empty set by A13;
A16: Q = { z where z is Element of Fi : X . i c= z } by A12, A13, A14, Th32;
X in bool M by MSSUBFAM:12;
then A17: X . i in (bool M) . i by A13;
consider f being Function of ((bool M) . i),((bool M) . i) such that
A18: f = J . i and
A19: for x being object st x in (bool M) . i holds
S₁[f . x,x,i] by A11, A13;
A20: S₁[f . (X . i),X . i,i] by A19, A17;
thus (J .. X) . i = f . (X . i) by A13, A18, PRALG_1:def 20
.= (meet SF) . i by A15, A16, A20 ; :: thesis:

end;

hence J .. X = meet SF ; :: thesis: