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]
then A4: M . i is finite by LL1;
A5: M . i <> {} by A3;
M . i is c=-linear

proof

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 A6: ( B' in M . i & C' in M . i ) ; :: thesis: R7(B',C')
assume A7: not B' c= C' ; :: according to XBOOLE_0:def 9 :: thesis: C' c= B'
consider b' being ManySortedSet of such that
A8: b' in M by PBOOLE:146;
consider c' being ManySortedSet of such that
A9: c' in M by PBOOLE:146;
set qb = b' +* (i .--> B');
set qc = c' +* (i .--> C');
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;
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;
A10: dom (i .--> B') = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A11: qb . i = (i .--> B') . i by A10, FUNCT_4:14
.= B' by FUNCOP_1:87 ;
A12: dom (i .--> C') = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A13: qc . i = (i .--> C') . i by A12, FUNCT_4:14
.= C' by FUNCOP_1:87 ;
A14: 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, A11; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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 A16: 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 A6, A13; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

end;

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

end;

consider m being ManySortedSet of such that
A18: 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 A18; :: 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 A19: 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 A20: i in I ; :: thesis: K . i c= m . i
then K . i in M . i by A19, PBOOLE:def 4;
hence K . i c= m . i by A18, A20; :: thesis: verum

end;