let I be set ; :: thesis:
let M be ManySortedSet of I; :: thesis:
let D be properly-upper-bound MSSubsetFamily of M; :: thesis:
let X be Element of bool M; :: thesis:
let SF be non-empty MSSubsetFamily of M; :: thesis:
assume A1: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ; :: thesis:
let i be set ; :: thesis:
let Di be non empty set ; :: thesis:
assume that
A2: i in I and
A3: Di = D . i ; :: thesis:
thus SF . i c= { z where z is Element of Di : X . i c= z } :: according to XBOOLE_0:def 10 :: thesis:

consider K being ManySortedSet of I such that
A4: K in SF by PBOOLE:134;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: x in SF . i ; :: thesis:
dom (K +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider L = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A6: dom (i .--> x) = {i} ;
i in {i} by TARSKI:def 1;
then A7: L . i = (i .--> x) . i by A6, FUNCT_4:13
.= x by FUNCOP_1:72 ;
A8: L in SF

let s be object ; :: according to PBOOLE:def 1 :: thesis:
assume A9: s in I ; :: thesis:

hence L . s in SF . s by A5, A7; :: thesis:

end;

end;

then X c= L by A1;
then A10: X . i c= L . i by A2;
L in D by A1, A8;
then L . i in D . i by A2;
hence x in { z where z is Element of Di : X . i c= z } by A3, A7, A10; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { z where z is Element of Di : X . i c= z } ; :: thesis:
then consider g being Element of Di such that
A11: g = x and
A12: X . i c= g ;
dom (M +* (i .--> g)) = I by A2, PZFMISC1:1;
then reconsider L1 = M +* (i .--> g) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A13: dom (i .--> g) = {i} ;
i in {i} by TARSKI:def 1;
then A14: L1 . i = (i .--> g) . i by A13, FUNCT_4:13
.= g by FUNCOP_1:72 ;
A15: X c= L1

let s be object ; :: according to PBOOLE:def 2 :: thesis:
assume A16: s in I ; :: thesis:

end;

end;

let s be object ; :: according to PBOOLE:def 1 :: thesis:
assume A20: s in I ; :: thesis:

end;

end;