let I be set ; :: thesis: for M being V8() V29() ManySortedSet of st ( for A, B being ManySortedSet of st A in M & B in M & not A c= B holds
B c= A ) holds
ex m being ManySortedSet of st
( m in M & ( for K being ManySortedSet of st K in M holds
K c= m ) )
let M be V8() V29() ManySortedSet of ; :: thesis: ( ( for A, B being ManySortedSet of st A in M & B in M & not A c= B holds
B c= A ) implies ex m being ManySortedSet of st
( m in M & ( for K being ManySortedSet of st K in M holds
K c= m ) ) )
assume A1: for A, B being ManySortedSet of st A in M & B in M & not A c= B holds
B c= A ; :: thesis: ex m being ManySortedSet of st
( m in M & ( for K being ManySortedSet of st K in M holds
K c= m ) )
defpred S₁[ set , set ] means ( $2 in M . $1 & ( for D' being set st D' in M . $1 holds
D' c= $2 ) );
A2: for i being set st i in I holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
assume A3: i in I ; :: thesis: ex j being set st S₁[i,j]
M . i is c=-linear

proof

consider c' being ManySortedSet of such that
A4: c' in M by PBOOLE:146;
consider b' being ManySortedSet of such that
A5: b' in M by PBOOLE:146;
let B', C' be set ; :: according to ORDINAL1:def 9 :: thesis: ( not B' in M . i or not C' in M . i or not R7(B',C') )
assume that
A6: B' in M . i and
A7: C' in M . i ; :: thesis: R7(B',C')
A8: dom (i .--> B') = {i} by FUNCOP_1:19;
set qc = c' +* (i .--> C');
dom (c' +* (i .--> C')) = I by A3, PZFMISC1:1;
then reconsider qc = c' +* (i .--> C') as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A9: dom (i .--> C') = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A10: qc . i = (i .--> C') . i by A9, FUNCT_4:14
.= C' by FUNCOP_1:87 ;
A11: qc in M

proof

let j be set ; :: according to PBOOLE:def 4 :: thesis: ( not j in I or qc . j in M . j )
assume A12: j in I ; :: thesis: qc . j in M . j

now

per cases ( j = i or j <> i ) ;

case j = i ; :: thesis: qc . j in M . j

hence qc . j in M . j by A7, A10; :: thesis: verum

end;

case j <> i ; :: thesis: qc . j in M . j

then not j in dom (i .--> C') by A9, TARSKI:def 1;
then qc . j = c' . j by FUNCT_4:12;
hence qc . j in M . j by A4, A12, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

hence qc . j in M . j ; :: thesis: verum

end;

set qb = b' +* (i .--> B');
dom (b' +* (i .--> B')) = I by A3, PZFMISC1:1;
then reconsider qb = b' +* (i .--> B') as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
assume A13: not B' c= C' ; :: according to XBOOLE_0:def 9 :: thesis: C' c= B'
i in {i} by TARSKI:def 1;
then A14: qb . i = (i .--> B') . i by A8, FUNCT_4:14
.= B' by FUNCOP_1:87 ;
qb in M

proof

let j be set ; :: according to PBOOLE:def 4 :: thesis: ( not j in I or qb . j in M . j )
assume A15: j in I ; :: thesis: qb . j in M . j

now

per cases ( j = i or j <> i ) ;

case j = i ; :: thesis: qb . j in M . j

hence qb . j in M . j by A6, A14; :: thesis: verum

end;

case j <> i ; :: thesis: qb . j in M . j

then not j in dom (i .--> B') by A8, TARSKI:def 1;
then qb . j = b' . j by FUNCT_4:12;
hence qb . j in M . j by A5, A15, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

hence qb . j in M . j ; :: thesis: verum

end;

then ( qb c= qc or qc c= qb ) by A1, A11;
hence C' c= B' by A3, A13, A14, A10, PBOOLE:def 5; :: thesis: verum

end;

then consider m' being set such that
A16: ( m' in M . i & ( for D' being set st D' in M . i holds
D' c= m' ) ) by A3, Lm1, FINSET_1:31;
take m' ; :: thesis: S₁[i,m']
thus S₁[i,m'] by A16; :: thesis: verum

end;

consider m being ManySortedSet of such that
A17: for i being set st i in I holds
S₁[i,m . i] from PBOOLE:sch 3(A2);
take m ; :: thesis: ( m in M & ( for K being ManySortedSet of st K in M holds
K c= m ) )
thus m in M :: thesis: for K being ManySortedSet of st K in M holds
K c= m

proof

let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or m . i in M . i )
assume i in I ; :: thesis: m . i in M . i
hence m . i in M . i by A17; :: thesis: verum

end;

thus for K being ManySortedSet of st K in M holds
K c= m :: thesis: verum

proof

let K be ManySortedSet of ; :: thesis: ( K in M implies K c= m )
assume A18: K in M ; :: thesis: K c= m
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or K . i c= m . i )
assume A19: i in I ; :: thesis: K . i c= m . i
then K . i in M . i by A18, PBOOLE:def 4;
hence K . i c= m . i by A17, A19; :: thesis: verum

end;