let I be set ; :: thesis: for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for X being Element of bool M ex SF being non-empty MSSubsetFamily of M st
for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )
let M be ManySortedSet of I; :: thesis: for D being properly-upper-bound MSSubsetFamily of M
for X being Element of bool M ex SF being non-empty MSSubsetFamily of M st
for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )
let D be properly-upper-bound MSSubsetFamily of M; :: thesis: for X being Element of bool M ex SF being non-empty MSSubsetFamily of M st
for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )
let X be Element of bool M; :: thesis: ex SF being non-empty MSSubsetFamily of M st
for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )
defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & X . $1 c= D2 );
consider SF being ManySortedSet of I such that
A1: for i being object st i in I holds
for e being object holds
( e in SF . i iff ( e in D . i & S₁[i,e] ) ) from PBOOLE:sch 2();
A2: D c= bool M by PBOOLE:def 18;
SF is ManySortedSubset of bool M

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in I or SF . i c= (bool M) . i )
assume A3: i in I ; :: thesis: SF . i c= (bool M) . i
then D . i c= (bool M) . i by A2;
then A4: D . i c= bool (M . i) by A3, MBOOLEAN:def 1;
SF . i c= bool (M . i)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SF . i or x in bool (M . i) )
assume x in SF . i ; :: thesis: x in bool (M . i)
then x in D . i by A1, A3;
hence x in bool (M . i) by A4; :: thesis: verum

end;

hence SF . i c= (bool M) . i by A3, MBOOLEAN:def 1; :: thesis: verum

end;

then reconsider SF = SF as ManySortedSubset of bool M ;
reconsider SF = SF as MSSubsetFamily of M ;
SF is non-empty

proof

let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not SF . i is empty )
assume A5: i in I ; :: thesis: not SF . i is empty
M in D by MSSUBFAM:def 6;
then A6: M . i in D . i by A5;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:18;
then X . i c= M . i by A5;
hence not SF . i is empty by A1, A5, A6; :: thesis: verum

end;

then reconsider SF = SF as non-empty MSSubsetFamily of M ;
take SF ; :: thesis: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )
let Y be ManySortedSet of I; :: thesis: ( Y in SF iff ( Y in D & X c= Y ) )
thus ( Y in SF implies ( Y in D & X c= Y ) ) :: thesis: ( Y in D & X c= Y implies Y in SF )

proof

assume A7: Y in SF ; :: thesis: ( Y in D & X c= Y )
thus Y in D :: thesis: X c= Y

proof

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or Y . i in D . i )
assume A8: i in I ; :: thesis: Y . i in D . i
then Y . i in SF . i by A7;
hence Y . i in D . i by A1, A8; :: thesis: verum

end;

thus X c= Y :: thesis: verum

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= Y . i )
assume A9: i in I ; :: thesis: X . i c= Y . i
then Y . i in SF . i by A7;
then ( Y . i in D . i & S₁[i,Y . i] ) by A1, A9;
hence X . i c= Y . i ; :: thesis: verum

end;

end;

assume A10: ( Y in D & X c= Y ) ; :: thesis: Y in SF
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or Y . i in SF . i )
assume A11: i in I ; :: thesis: Y . i in SF . i
then ( Y . i in D . i & X . i c= Y . i ) by A10;
hence Y . i in SF . i by A1, A11; :: thesis: verum