let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) holds
for x, y being Element of () holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )

let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) implies for x, y being Element of () holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) ) )

set L = product J;
assume A1: for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ; :: thesis: for x, y being Element of () holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )

then reconsider L9 = product J as non empty up-complete Poset by Th11;
let x, y be Element of (); :: thesis: ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )

hereby :: thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) implies x << y )
assume A2: x << y ; :: thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) )

hereby :: thesis: ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i)
let i be Element of I; :: thesis: x . i << y . i
thus x . i << y . i :: thesis: verum
proof
let Di be non empty directed Subset of (J . i); :: according to WAYBEL_3:def 1 :: thesis: ( not y . i <= "\/" (Di,(J . i)) or ex b1 being Element of the carrier of (J . i) st
( b1 in Di & x . i <= b1 ) )

assume A3: y . i <= sup Di ; :: thesis: ex b1 being Element of the carrier of (J . i) st
( b1 in Di & x . i <= b1 )

set di = the Element of Di;
set D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } ;
reconsider di = the Element of Di as Element of (J . i) ;
A4: dom y = I by WAYBEL_3:27;
{ (y +* (i,z)) where z is Element of (J . i) : z in Di } c= the carrier of ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (y +* (i,z)) where z is Element of (J . i) : z in Di } or a in the carrier of () )
assume a in { (y +* (i,z)) where z is Element of (J . i) : z in Di } ; :: thesis: a in the carrier of ()
then consider z being Element of (J . i) such that
A5: a = y +* (i,z) and
z in Di ;
A6: now :: thesis: for j being Element of I holds (y +* (i,z)) . j is Element of (J . j)
let j be Element of I; :: thesis: (y +* (i,z)) . j is Element of (J . j)
( i = j or i <> j ) ;
then ( ( (y +* (i,z)) . j = z & i = j ) or (y +* (i,z)) . j = y . j ) by ;
hence (y +* (i,z)) . j is Element of (J . j) ; :: thesis: verum
end;
dom (y +* (i,z)) = I by ;
then a is Element of () by ;
hence a in the carrier of () ; :: thesis: verum
end;
then reconsider D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } as Subset of () ;
A7: y +* (i,di) in D ;
then reconsider D = D as non empty Subset of () ;
D is directed
proof
let z1, z2 be Element of (); :: according to WAYBEL_0:def 1 :: thesis: ( not z1 in D or not z2 in D or ex b1 being Element of the carrier of () st
( b1 in D & z1 <= b1 & z2 <= b1 ) )

assume z1 in D ; :: thesis: ( not z2 in D or ex b1 being Element of the carrier of () st
( b1 in D & z1 <= b1 & z2 <= b1 ) )

then consider a1 being Element of (J . i) such that
A8: z1 = y +* (i,a1) and
A9: a1 in Di ;
assume z2 in D ; :: thesis: ex b1 being Element of the carrier of () st
( b1 in D & z1 <= b1 & z2 <= b1 )

then consider a2 being Element of (J . i) such that
A10: z2 = y +* (i,a2) and
A11: a2 in Di ;
consider a being Element of (J . i) such that
A12: a in Di and
A13: a >= a1 and
A14: a >= a2 by ;
y +* (i,a) in D by A12;
then reconsider z = y +* (i,a) as Element of () ;
take z ; :: thesis: ( z in D & z1 <= z & z2 <= z )
thus z in D by A12; :: thesis: ( z1 <= z & z2 <= z )
A15: dom y = I by WAYBEL_3:27;
now :: thesis: for j being Element of I holds z . j >= z1 . j
let j be Element of I; :: thesis: z . j >= z1 . j
( i = j or i <> j ) ;
then ( ( z . j = a & z1 . j = a1 & i = j ) or ( z . j = y . j & z1 . j = y . j ) ) by ;
hence z . j >= z1 . j by ; :: thesis: verum
end;
hence z >= z1 by WAYBEL_3:28; :: thesis: z2 <= z
now :: thesis: for j being Element of I holds z . j >= z2 . j
let j be Element of I; :: thesis: z . j >= z2 . j
( i = j or i <> j ) ;
then ( ( z . j = a & z2 . j = a2 & i = j ) or ( z . j = y . j & z2 . j = y . j ) ) by ;
hence z . j >= z2 . j by ; :: thesis: verum
end;
hence z2 <= z by WAYBEL_3:28; :: thesis: verum
end;
then reconsider D = D as non empty directed Subset of () ;
A16: dom y = I by WAYBEL_3:27;
now :: thesis: for j being Element of I holds (sup D) . j >= y . j
A17: Di c= pi (D,i)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Di or a in pi (D,i) )
assume A18: a in Di ; :: thesis: a in pi (D,i)
then reconsider a = a as Element of (J . i) ;
y +* (i,a) in D by A18;
then (y +* (i,a)) . i in pi (D,i) by CARD_3:def 6;
hence a in pi (D,i) by ; :: thesis: verum
end;
let j be Element of I; :: thesis: (sup D) . j >= y . j
A19: ( J . i is non empty up-complete Poset & J . j is non empty up-complete Poset ) by A1;
( not pi (D,i) is empty & pi (D,i) is directed ) by YELLOW16:35;
then A20: ex_sup_of pi (D,i),J . i by ;
ex_sup_of Di,J . i by ;
then A21: sup Di <= sup (pi (D,i)) by ;
ex_sup_of D,L9 by WAYBEL_0:75;
then A22: (sup D) . j = sup (pi (D,j)) by YELLOW16:33;
A23: now :: thesis: ( j <> i implies y . j in pi (D,j) )
assume j <> i ; :: thesis: y . j in pi (D,j)
then (y +* (i,di)) . j = y . j by FUNCT_7:32;
hence y . j in pi (D,j) by ; :: thesis: verum
end;
( not pi (D,j) is empty & pi (D,j) is directed ) by YELLOW16:35;
then ex_sup_of pi (D,j),J . j by ;
then (sup D) . j is_>=_than pi (D,j) by ;
hence (sup D) . j >= y . j by ; :: thesis: verum
end;
then sup D >= y by WAYBEL_3:28;
then consider d being Element of () such that
A24: d in D and
A25: d >= x by A2;
consider z being Element of (J . i) such that
A26: d = y +* (i,z) and
A27: z in Di by A24;
take z ; :: thesis: ( z in Di & x . i <= z )
d . i = z by ;
hence ( z in Di & x . i <= z ) by ; :: thesis: verum
end;
end;
set K = { i where i is Element of I : x . i <> Bottom (J . i) } ;
{ i where i is Element of I : x . i <> Bottom (J . i) } c= I
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { i where i is Element of I : x . i <> Bottom (J . i) } or a in I )
assume a in { i where i is Element of I : x . i <> Bottom (J . i) } ; :: thesis: a in I
then ex i being Element of I st
( a = i & x . i <> Bottom (J . i) ) ;
hence a in I ; :: thesis: verum
end;
then reconsider K = { i where i is Element of I : x . i <> Bottom (J . i) } as Subset of I ;
deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = Bottom (J . \$1);
consider f being ManySortedSet of I such that
A28: for i being Element of I holds f . i = H1(i) from PBOOLE:sch 5();
A29: now :: thesis: for i being Element of I holds f . i is Element of (J . i)
let i be Element of I; :: thesis: f . i is Element of (J . i)
f . i = Bottom (J . i) by A28;
hence f . i is Element of (J . i) ; :: thesis: verum
end;
A30: dom f = I by PARTFUN1:def 2;
then reconsider f = f as Element of () by ;
set X = { (f +* (y | a)) where a is finite Subset of I : verum } ;
{ (f +* (y | a)) where a is finite Subset of I : verum } c= the carrier of ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (f +* (y | a)) where a is finite Subset of I : verum } or a in the carrier of () )
assume a in { (f +* (y | a)) where a is finite Subset of I : verum } ; :: thesis: a in the carrier of ()
then consider b being finite Subset of I such that
A31: a = f +* (y | b) ;
dom y = I by WAYBEL_3:27;
then A32: dom (y | b) = b by RELAT_1:62;
A33: now :: thesis: for i being Element of I holds (f +* (y | b)) . i is Element of (J . i)
let i be Element of I; :: thesis: (f +* (y | b)) . i is Element of (J . i)
( (f +* (y | b)) . i = f . i or ( (f +* (y | b)) . i = (y | b) . i & (y | b) . i = y . i ) ) by ;
hence (f +* (y | b)) . i is Element of (J . i) ; :: thesis: verum
end;
I = I \/ (dom (y | b)) by
.= dom (f +* (y | b)) by ;
then a is Element of () by ;
hence a in the carrier of () ; :: thesis: verum
end;
then reconsider X = { (f +* (y | a)) where a is finite Subset of I : verum } as Subset of () ;
f +* (y | ({} I)) in X ;
then reconsider X = X as non empty Subset of () ;
X is directed
proof
let z1, z2 be Element of (); :: according to WAYBEL_0:def 1 :: thesis: ( not z1 in X or not z2 in X or ex b1 being Element of the carrier of () st
( b1 in X & z1 <= b1 & z2 <= b1 ) )

assume z1 in X ; :: thesis: ( not z2 in X or ex b1 being Element of the carrier of () st
( b1 in X & z1 <= b1 & z2 <= b1 ) )

then consider a1 being finite Subset of I such that
A34: z1 = f +* (y | a1) ;
assume z2 in X ; :: thesis: ex b1 being Element of the carrier of () st
( b1 in X & z1 <= b1 & z2 <= b1 )

then consider a2 being finite Subset of I such that
A35: z2 = f +* (y | a2) ;
reconsider a = a1 \/ a2 as finite Subset of I ;
f +* (y | a) in X ;
then reconsider z = f +* (y | a) as Element of () ;
take z ; :: thesis: ( z in X & z1 <= z & z2 <= z )
thus z in X ; :: thesis: ( z1 <= z & z2 <= z )
A36: dom y = I by WAYBEL_3:27;
then A37: dom (y | a) = a by RELAT_1:62;
A38: dom (y | a1) = a1 by ;
now :: thesis: for i being Element of I holds z . i >= z1 . i
let i be Element of I; :: thesis: z . b1 >= z1 . b1
A39: f . i = Bottom (J . i) by A28;
J . i is non empty lower-bounded up-complete Poset by A1;
then A40: Bottom (J . i) <= y . i by YELLOW_0:44;
per cases ( ( not i in a1 & i in a ) or ( not i in a & not i in a1 ) or ( i in a1 & i in a ) ) by XBOOLE_0:def 3;
suppose A41: ( not i in a1 & i in a ) ; :: thesis: z . b1 >= z1 . b1
then ( z . i = (y | a) . i & (y | a) . i = y . i ) by ;
hence z . i >= z1 . i by ; :: thesis: verum
end;
suppose ( not i in a & not i in a1 ) ; :: thesis: z . b1 >= z1 . b1
then ( z . i = f . i & z1 . i = f . i ) by ;
hence z . i >= z1 . i by YELLOW_0:def 1; :: thesis: verum
end;
suppose A42: ( i in a1 & i in a ) ; :: thesis: z . b1 >= z1 . b1
then A43: ( z . i = (y | a) . i & (y | a) . i = y . i ) by ;
( z1 . i = (y | a1) . i & (y | a1) . i = y . i ) by ;
hence z . i >= z1 . i by ; :: thesis: verum
end;
end;
end;
hence z >= z1 by WAYBEL_3:28; :: thesis: z2 <= z
A44: dom (y | a2) = a2 by ;
now :: thesis: for i being Element of I holds z . i >= z2 . i
let i be Element of I; :: thesis: z . b1 >= z2 . b1
A45: f . i = Bottom (J . i) by A28;
J . i is non empty lower-bounded up-complete Poset by A1;
then A46: Bottom (J . i) <= y . i by YELLOW_0:44;
per cases ( ( not i in a2 & i in a ) or ( not i in a & not i in a2 ) or ( i in a2 & i in a ) ) by XBOOLE_0:def 3;
suppose A47: ( not i in a2 & i in a ) ; :: thesis: z . b1 >= z2 . b1
then ( z . i = (y | a) . i & (y | a) . i = y . i ) by ;
hence z . i >= z2 . i by ; :: thesis: verum
end;
suppose ( not i in a & not i in a2 ) ; :: thesis: z . b1 >= z2 . b1
then ( z . i = f . i & z2 . i = f . i ) by ;
hence z . i >= z2 . i by YELLOW_0:def 1; :: thesis: verum
end;
suppose A48: ( i in a2 & i in a ) ; :: thesis: z . b1 >= z2 . b1
then A49: ( z . i = (y | a) . i & (y | a) . i = y . i ) by ;
( z2 . i = (y | a2) . i & (y | a2) . i = y . i ) by ;
hence z . i >= z2 . i by ; :: thesis: verum
end;
end;
end;
hence z2 <= z by WAYBEL_3:28; :: thesis: verum
end;
then reconsider X = X as non empty directed Subset of () ;
now :: thesis: for i being Element of I holds (sup X) . i >= y . i
let i be Element of I; :: thesis: (sup X) . i >= y . i
reconsider a = {i} as finite Subset of I by ZFMISC_1:31;
A50: f +* (y | a) in X ;
then reconsider z = f +* (y | a) as Element of () ;
ex_sup_of X,L9 by WAYBEL_0:75;
then sup X is_>=_than X by YELLOW_0:30;
then A51: z <= sup X by A50;
dom y = I by WAYBEL_3:27;
then A52: dom (y | a) = a by RELAT_1:62;
A53: i in a by TARSKI:def 1;
then (y | a) . i = y . i by FUNCT_1:49;
then z . i = y . i by ;
hence (sup X) . i >= y . i by ; :: thesis: verum
end;
then y <= sup X by WAYBEL_3:28;
then consider d being Element of () such that
A54: d in X and
A55: x <= d by A2;
consider a being finite Subset of I such that
A56: d = f +* (y | a) by A54;
K c= a
proof
dom y = I by WAYBEL_3:27;
then A57: dom (y | a) = a by RELAT_1:62;
let j be object ; :: according to TARSKI:def 3 :: thesis: ( not j in K or j in a )
assume j in K ; :: thesis: j in a
then consider i being Element of I such that
A58: j = i and
A59: x . i <> Bottom (J . i) ;
J . i is non empty lower-bounded up-complete Poset by A1;
then A60: x . i >= Bottom (J . i) by YELLOW_0:44;
assume not j in a ; :: thesis: contradiction
then A61: d . i = f . i by
.= Bottom (J . i) by A28 ;
x . i <= d . i by ;
hence contradiction by A59, A61, A60, ORDERS_2:2; :: thesis: verum
end;
then reconsider K = K as finite Subset of I ;
take K = K; :: thesis: for i being Element of I st not i in K holds
x . i = Bottom (J . i)

thus for i being Element of I st not i in K holds
x . i = Bottom (J . i) ; :: thesis: verum
end;
defpred S1[ object , object ] means ex i being Element of I ex z being Element of () st
( \$1 = i & \$2 = z & z . i >= x . i );
assume A62: for i being Element of I holds x . i << y . i ; :: thesis: ( for K being finite Subset of I ex i being Element of I st
( not i in K & not x . i = Bottom (J . i) ) or x << y )

given K being finite Subset of I such that A63: for i being Element of I st not i in K holds
x . i = Bottom (J . i) ; :: thesis: x << y
let D be non empty directed Subset of (); :: according to WAYBEL_3:def 1 :: thesis: ( not y <= "\/" (D,()) or ex b1 being Element of the carrier of () st
( b1 in D & x <= b1 ) )

assume A64: y <= sup D ; :: thesis: ex b1 being Element of the carrier of () st
( b1 in D & x <= b1 )

A65: now :: thesis: for k being object st k in K holds
ex a being object st
( a in D & S1[k,a] )
let k be object ; :: thesis: ( k in K implies ex a being object st
( a in D & S1[k,a] ) )

assume k in K ; :: thesis: ex a being object st
( a in D & S1[k,a] )

then reconsider i = k as Element of I ;
A66: pi (D,i) is directed
proof
let a, b be Element of (J . i); :: according to WAYBEL_0:def 1 :: thesis: ( not a in pi (D,i) or not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )

assume a in pi (D,i) ; :: thesis: ( not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )

then consider f being Function such that
A67: f in D and
A68: a = f . i by CARD_3:def 6;
assume b in pi (D,i) ; :: thesis: ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 )

then consider g being Function such that
A69: g in D and
A70: b = g . i by CARD_3:def 6;
reconsider f = f, g = g as Element of () by ;
consider h being Element of () such that
A71: ( h in D & h >= f & h >= g ) by ;
take h . i ; :: thesis: ( h . i in pi (D,i) & a <= h . i & b <= h . i )
thus ( h . i in pi (D,i) & a <= h . i & b <= h . i ) by ; :: thesis: verum
end;
ex_sup_of D,L9 by WAYBEL_0:75;
then A72: (sup D) . i = sup (pi (D,i)) by YELLOW16:33;
( x . i << y . i & y . i <= (sup D) . i ) by ;
then consider zi being Element of (J . i) such that
A73: zi in pi (D,i) and
A74: zi >= x . i by ;
consider a being Function such that
A75: a in D and
A76: zi = a . i by ;
reconsider a = a as object ;
take a = a; :: thesis: ( a in D & S1[k,a] )
thus a in D by A75; :: thesis: S1[k,a]
thus S1[k,a] by A74, A75, A76; :: thesis: verum
end;
consider F being Function such that
A77: ( dom F = K & rng F c= D ) and
A78: for k being object st k in K holds
S1[k,F . k] from reconsider Y = rng F as finite Subset of D by ;
consider d being Element of () such that
A79: d in D and
A80: d is_>=_than Y by WAYBEL_0:1;
take d ; :: thesis: ( d in D & x <= d )
thus d in D by A79; :: thesis: x <= d
now :: thesis: for i being Element of I holds d . i >= x . i
let i be Element of I; :: thesis: d . b1 >= x . b1
A81: J . i is non empty lower-bounded up-complete Poset by A1;
per cases ( i in K or not i in K ) ;
suppose A82: i in K ; :: thesis: d . b1 >= x . b1
then consider j being Element of I, z being Element of () such that
A83: i = j and
A84: F . i = z and
A85: z . j >= x . j by A78;
z in Y by ;
then d >= z by A80;
then d . i >= z . i by WAYBEL_3:28;
hence d . i >= x . i by ; :: thesis: verum
end;
suppose not i in K ; :: thesis: d . b1 >= x . b1
then x . i = Bottom (J . i) by A63;
hence d . i >= x . i by ; :: thesis: verum
end;
end;
end;
hence x <= d by WAYBEL_3:28; :: thesis: verum