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

proof

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

proof

consider c9 being ManySortedSet of I such that
A4: c9 in M by PBOOLE:134;
consider b9 being ManySortedSet of I such that
A5: b9 in M by PBOOLE:134;
let B9, C9 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not B9 in M . i or not C9 in M . i or B9,C9 are_c=-comparable )
assume that
A6: B9 in M . i and
A7: C9 in M . i ; :: thesis: B9,C9 are_c=-comparable
A8: dom (i .--> B9) = {i} ;
set qc = c9 +* (i .--> C9);
dom (c9 +* (i .--> C9)) = I by A3, PZFMISC1:1;
then reconsider qc = c9 +* (i .--> C9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A9: dom (i .--> C9) = {i} ;
i in {i} by TARSKI:def 1;
then A10: qc . i = (i .--> C9) . i by A9, FUNCT_4:13
.= C9 by FUNCOP_1:72 ;
A11: qc in M

proof

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

now :: thesis: ( ( j = i & qc . j in M . j ) or ( j <> i & qc . j in M . j ) )

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 .--> C9) by TARSKI:def 1;
then qc . j = c9 . j by FUNCT_4:11;
hence qc . j in M . j by A4, A12; :: thesis: verum

end;

end;

end;

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

end;

set qb = b9 +* (i .--> B9);
dom (b9 +* (i .--> B9)) = I by A3, PZFMISC1:1;
then reconsider qb = b9 +* (i .--> B9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
assume A13: not B9 c= C9 ; :: according to XBOOLE_0:def 9 :: thesis: C9 c= B9
i in {i} by TARSKI:def 1;
then A14: qb . i = (i .--> B9) . i by A8, FUNCT_4:13
.= B9 by FUNCOP_1:72 ;
qb in M

proof

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

now :: thesis: ( ( j = i & qb . j in M . j ) or ( j <> i & qb . j in M . j ) )

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 .--> B9) by TARSKI:def 1;
then qb . j = b9 . j by FUNCT_4:11;
hence qb . j in M . j by A5, A15; :: 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 C9 c= B9 by A3, A13, A14, A10; :: thesis: verum

end;

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

end;

consider m being ManySortedSet of I such that
A17: for i being object 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 I st K in M holds
m c= K ) )
thus m in M :: thesis: for K being ManySortedSet of I st K in M holds
m c= K

proof

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or m . i in M . i )
assume i in I ; :: thesis: m . i in M . i
then S₁[i,m . i] by A17;
hence m . i in M . i ; :: thesis: verum

end;

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

proof

let C be ManySortedSet of I; :: thesis: ( C in M implies m c= C )
assume A18: C in M ; :: thesis: m c= C
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or m . i c= C . i )
assume A19: i in I ; :: thesis: m . i c= C . i
then A20: C . i in M . i by A18;
S₁[i,m . i] by A17, A19;
hence m . i c= C . i by A20; :: thesis: verum

end;