let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for x, y being Element of (product J) 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 RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for x, y being Element of (product J) 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 complete LATTICE ; :: thesis: for x, y being Element of (product J) 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 complete LATTICE by Th31;
let x, y be Element of (product J); :: 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
not 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
not 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: ( y . i <= sup Di implies ex d being Element of (J . i) st
( d in Di & x . i <= d ) )
assume A3: y . i <= sup Di ; :: thesis: ex d being Element of (J . i) st
( d in Di & x . i <= d )
A4: dom y = I by Th27;
set D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } ;
{ (y +* (i,z)) where z is Element of (J . i) : z in Di } c= the carrier of (product J)

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 (product J) )
assume a in { (y +* (i,z)) where z is Element of (J . i) : z in Di } ; :: thesis: a in the carrier of (product J)
then consider z being Element of (J . i) such that
A5: a = y +* (i,z) and
z in Di ;
A6: dom (y +* (i,z)) = I by A4, FUNCT_7:30;

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 A4, FUNCT_7:31, FUNCT_7:32;
hence (y +* (i,z)) . j is Element of (J . j) ; :: thesis: verum

end;

then a is Element of (product J) by A5, A6, Th27;
hence a in the carrier of (product J) ; :: thesis: verum

end;

then reconsider D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } as Subset of (product J) ;
set di = the Element of Di;
reconsider di = the Element of Di as Element of (J . i) ;
A7: y +* (i,di) in D ;
A8: dom y = I by Th27;
reconsider D = D as non empty Subset of (product J) by A7;
D is directed

proof

let z1, z2 be Element of (product J); :: according to WAYBEL_0:def 1 :: thesis: ( not z1 in D or not z2 in D or ex b₁ being Element of the carrier of (product J) st
( b₁ in D & z1 <= b₁ & z2 <= b₁ ) )
assume z1 in D ; :: thesis: ( not z2 in D or ex b₁ being Element of the carrier of (product J) st
( b₁ in D & z1 <= b₁ & z2 <= b₁ ) )
then consider a1 being Element of (J . i) such that
A9: z1 = y +* (i,a1) and
A10: a1 in Di ;
assume z2 in D ; :: thesis: ex b₁ being Element of the carrier of (product J) st
( b₁ in D & z1 <= b₁ & z2 <= b₁ )
then consider a2 being Element of (J . i) such that
A11: z2 = y +* (i,a2) and
A12: a2 in Di ;
consider a being Element of (J . i) such that
A13: a in Di and
A14: a >= a1 and
A15: a >= a2 by A10, A12, WAYBEL_0:def 1;
y +* (i,a) in D by A13;
then reconsider z = y +* (i,a) as Element of (product J) ;
take z ; :: thesis: ( z in D & z1 <= z & z2 <= z )
thus z in D by A13; :: thesis: ( z1 <= z & z2 <= z )
A16: dom y = I by Th27;

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 A9, A16, FUNCT_7:31, FUNCT_7:32;
hence z . j >= z1 . j by A14, YELLOW_0:def 1; :: thesis: verum

end;

hence z >= z1 by Th28; :: 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 A11, A16, FUNCT_7:31, FUNCT_7:32;
hence z . j >= z2 . j by A15, YELLOW_0:def 1; :: thesis: verum

end;

hence z2 <= z by Th28; :: thesis: verum

end;

then reconsider D = D as non empty directed Subset of (product J) ;

now :: thesis: for j being Element of I holds (sup D) . j >= y . j

let j be Element of I; :: thesis: (sup D) . j >= y . j
A17: J . i is complete LATTICE by A1;
A18: J . j is complete LATTICE by A1;
A19: ex_sup_of Di,J . i by A17, YELLOW_0:17;
A20: ex_sup_of pi (D,i),J . i by A17, YELLOW_0:17;
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 A21: a in Di ; :: thesis: a in pi (D,i)
then reconsider a = a as Element of (J . i) ;
y +* (i,a) in D by A21;
then (y +* (i,a)) . i in pi (D,i) by CARD_3:def 6;
hence a in pi (D,i) by A8, FUNCT_7:31; :: thesis: verum

end;

then A22: sup Di <= sup (pi (D,i)) by A19, A20, YELLOW_0:34;
A23: (sup D) . j = sup (pi (D,j)) by A1, Th32;

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 A7, CARD_3:def 6; :: thesis: verum

end;

hence (sup D) . j >= y . j by A3, A18, A22, A23, YELLOW_0:def 2, YELLOW_2:22; :: thesis: verum

end;

then sup D >= y by Th28;
then consider d being Element of (product J) 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 A4, A26, FUNCT_7:31;
hence ( z in Di & x . i <= z ) by A25, A27, Th28; :: 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 H₁( 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 = H₁(i) from PBOOLE:sch 5();
A29: dom f = I by PARTFUN1:def 2;

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;

then reconsider f = f as Element of (product J) by A29, Th27;
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 (product J)

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 (product J) )
assume a in { (f +* (y | a)) where a is finite Subset of I : verum } ; :: thesis: a in the carrier of (product J)
then consider b being finite Subset of I such that
A30: a = f +* (y | b) ;
dom y = I by Th27;
then A31: dom (y | b) = b by RELAT_1:62;
then A32: I = I \/ (dom (y | b)) by XBOOLE_1:12
.= dom (f +* (y | b)) by A29, FUNCT_4:def 1 ;

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 A31, FUNCT_1:47, FUNCT_4:11, FUNCT_4:13;
hence (f +* (y | b)) . i is Element of (J . i) ; :: thesis: verum

end;

then a is Element of (product J) by A30, A32, Th27;
hence a in the carrier of (product J) ; :: thesis: verum

end;

then reconsider X = { (f +* (y | a)) where a is finite Subset of I : verum } as Subset of (product J) ;
f +* (y | ({} I)) in X ;
then reconsider X = X as non empty Subset of (product J) ;
X is directed

proof

let z1, z2 be Element of (product J); :: according to WAYBEL_0:def 1 :: thesis: ( not z1 in X or not z2 in X or ex b₁ being Element of the carrier of (product J) st
( b₁ in X & z1 <= b₁ & z2 <= b₁ ) )
assume z1 in X ; :: thesis: ( not z2 in X or ex b₁ being Element of the carrier of (product J) st
( b₁ in X & z1 <= b₁ & z2 <= b₁ ) )
then consider a1 being finite Subset of I such that
A33: z1 = f +* (y | a1) ;
assume z2 in X ; :: thesis: ex b₁ being Element of the carrier of (product J) st
( b₁ in X & z1 <= b₁ & z2 <= b₁ )
then consider a2 being finite Subset of I such that
A34: 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 (product J) ;
take z ; :: thesis: ( z in X & z1 <= z & z2 <= z )
thus z in X ; :: thesis: ( z1 <= z & z2 <= z )
A35: dom y = I by Th27;
then A36: dom (y | a) = a by RELAT_1:62;
A37: dom (y | a1) = a1 by A35, RELAT_1:62;
A38: dom (y | a2) = a2 by A35, RELAT_1:62;

now :: thesis: for i being Element of I holds z . i >= z1 . i

let i be Element of I; :: thesis: z . b₁ >= z1 . b₁
J . i is complete LATTICE by A1;
then A39: Bottom (J . i) <= y . i by YELLOW_0:44;
A40: f . i = Bottom (J . i) by A28;

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 . b₁ >= z1 . b₁

then A42: z . i = (y | a) . i by A36, FUNCT_4:13;
(y | a) . i = y . i by A36, A41, FUNCT_1:47;
hence z . i >= z1 . i by A33, A37, A39, A40, A41, A42, FUNCT_4:11; :: thesis: verum

end;

suppose A43: ( not i in a & not i in a1 ) ; :: thesis: z . b₁ >= z1 . b₁

then A44: z . i = f . i by A36, FUNCT_4:11;
z1 . i = f . i by A33, A37, A43, FUNCT_4:11;
hence z . i >= z1 . i by A44, YELLOW_0:def 1; :: thesis: verum

end;

suppose A45: ( i in a1 & i in a ) ; :: thesis: z . b₁ >= z1 . b₁

then A46: z . i = (y | a) . i by A36, FUNCT_4:13;
A47: (y | a) . i = y . i by A36, A45, FUNCT_1:47;
A48: z1 . i = (y | a1) . i by A33, A37, A45, FUNCT_4:13;
(y | a1) . i = y . i by A37, A45, FUNCT_1:47;
hence z . i >= z1 . i by A46, A47, A48, YELLOW_0:def 1; :: thesis: verum

end;

end;

end;

hence z >= z1 by Th28; :: thesis: z2 <= z

now :: thesis: for i being Element of I holds z . i >= z2 . i

let i be Element of I; :: thesis: z . b₁ >= z2 . b₁
J . i is complete LATTICE by A1;
then A49: Bottom (J . i) <= y . i by YELLOW_0:44;
A50: f . i = Bottom (J . i) by A28;

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 A51: ( not i in a2 & i in a ) ; :: thesis: z . b₁ >= z2 . b₁

then A52: z . i = (y | a) . i by A36, FUNCT_4:13;
(y | a) . i = y . i by A36, A51, FUNCT_1:47;
hence z . i >= z2 . i by A34, A38, A49, A50, A51, A52, FUNCT_4:11; :: thesis: verum

end;

suppose A53: ( not i in a & not i in a2 ) ; :: thesis: z . b₁ >= z2 . b₁

then A54: z . i = f . i by A36, FUNCT_4:11;
z2 . i = f . i by A34, A38, A53, FUNCT_4:11;
hence z . i >= z2 . i by A54, YELLOW_0:def 1; :: thesis: verum

end;

suppose A55: ( i in a2 & i in a ) ; :: thesis: z . b₁ >= z2 . b₁

then A56: z . i = (y | a) . i by A36, FUNCT_4:13;
A57: (y | a) . i = y . i by A36, A55, FUNCT_1:47;
A58: z2 . i = (y | a2) . i by A34, A38, A55, FUNCT_4:13;
(y | a2) . i = y . i by A38, A55, FUNCT_1:47;
hence z . i >= z2 . i by A56, A57, A58, YELLOW_0:def 1; :: thesis: verum

end;

end;

end;

hence z2 <= z by Th28; :: thesis: verum

end;

then reconsider X = X as non empty directed Subset of (product J) ;

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 ;
A59: f +* (y | a) in X ;
A60: product J = L9 ;
reconsider z = f +* (y | a) as Element of (product J) by A59;
A61: dom y = I by Th27;
A62: i in a by TARSKI:def 1;
then A63: (y | a) . i = y . i by FUNCT_1:49;
A64: dom (y | a) = a by A61, RELAT_1:62;
A65: z <= sup X by A59, A60, YELLOW_2:22;
z . i = y . i by A62, A63, A64, FUNCT_4:13;
hence (sup X) . i >= y . i by A65, Th28; :: thesis: verum

end;

then y <= sup X by Th28;
then consider d being Element of (product J) such that
A66: d in X and
A67: x <= d by A2;
consider a being finite Subset of I such that
A68: d = f +* (y | a) by A66;
K c= a

proof

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
A69: j = i and
A70: x . i <> Bottom (J . i) ;
assume A71: not j in a ; :: thesis: contradiction
dom y = I by Th27;
then dom (y | a) = a by RELAT_1:62;
then A72: d . i = f . i by A68, A69, A71, FUNCT_4:11
.= Bottom (J . i) by A28 ;
A73: J . i is complete LATTICE by A1;
A74: x . i <= d . i by A67, Th28;
x . i >= Bottom (J . i) by A73, YELLOW_0:44;
hence contradiction by A70, A72, A73, A74, 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
not x . i <> Bottom (J . i)
thus for i being Element of I st not i in K holds
not x . i <> Bottom (J . i) ; :: thesis: verum

end;

assume A75: 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 A76: 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 (product J); :: according to WAYBEL_3:def 1 :: thesis: ( y <= sup D implies ex d being Element of (product J) st
( d in D & x <= d ) )
assume A77: y <= sup D ; :: thesis: ex d being Element of (product J) st
( d in D & x <= d )
defpred S₁[ object , object ] means ex i being Element of I ex z being Element of (product J) st
( $1 = i & $2 = z & z . i >= x . i );

A78: now :: thesis: for k being object st k in K holds
ex a being object st
( a in D & S₁[k,a] )

let k be object ; :: thesis: ( k in K implies ex a being object st
( a in D & S₁[k,a] ) )
assume k in K ; :: thesis: ex a being object st
( a in D & S₁[k,a] )
then reconsider i = k as Element of I ;
A79: 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 b₁ being Element of the carrier of (J . i) st
( b₁ in pi (D,i) & a <= b₁ & b <= b₁ ) )
assume a in pi (D,i) ; :: thesis: ( not b in pi (D,i) or ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi (D,i) & a <= b₁ & b <= b₁ ) )
then consider f being Function such that
A80: f in D and
A81: a = f . i by CARD_3:def 6;
assume b in pi (D,i) ; :: thesis: ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi (D,i) & a <= b₁ & b <= b₁ )
then consider g being Function such that
A82: g in D and
A83: b = g . i by CARD_3:def 6;
reconsider f = f, g = g as Element of (product J) by A80, A82;
consider h being Element of (product J) such that
A84: h in D and
A85: h >= f and
A86: h >= g by A80, A82, WAYBEL_0:def 1;
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 A81, A83, A84, A85, A86, Th28, CARD_3:def 6; :: thesis: verum

end;

set dd = the Element of D;
reconsider dd = the Element of D as Element of (product J) ;
A87: dd . i in pi (D,i) by CARD_3:def 6;
A88: x . i << y . i by A75;
A89: y . i <= (sup D) . i by A77, Th28;
(sup D) . i = sup (pi (D,i)) by A1, Th32;
then consider zi being Element of (J . i) such that
A90: zi in pi (D,i) and
A91: zi >= x . i by A79, A87, A88, A89;
consider a being Function such that
A92: a in D and
A93: zi = a . i by A90, CARD_3:def 6;
reconsider a = a as object ;
take a = a; :: thesis: ( a in D & S₁[k,a] )
thus a in D by A92; :: thesis: S₁[k,a]
thus S₁[k,a] by A91, A92, A93; :: thesis: verum

end;

consider F being Function such that
A94: ( dom F = K & rng F c= D ) and
A95: for k being object st k in K holds
S₁[k,F . k] from FUNCT_1:sch 6(A78);
reconsider Y = rng F as finite Subset of D by A94, FINSET_1:8;
product J = L9 ;
then consider d being Element of (product J) such that
A96: d in D and
A97: d is_>=_than Y by WAYBEL_0:1;
take d ; :: thesis: ( d in D & x <= d )
thus d in D by A96; :: thesis: x <= d

now :: thesis: for i being Element of I holds d . i >= x . i

let i be Element of I; :: thesis: d . b₁ >= x . b₁
A98: J . i is complete LATTICE by A1;

per cases ( i in K or not i in K ) ;

suppose A99: i in K ; :: thesis: d . b₁ >= x . b₁

then consider j being Element of I, z being Element of (product J) such that
A100: i = j and
A101: F . i = z and
A102: z . j >= x . j by A95;
z in Y by A94, A99, A101, FUNCT_1:def 3;
then d >= z by A97;
then d . i >= z . i by Th28;
hence d . i >= x . i by A98, A100, A102, YELLOW_0:def 2; :: thesis: verum

end;

suppose not i in K ; :: thesis: d . b₁ >= x . b₁

then x . i = Bottom (J . i) by A76;
hence d . i >= x . i by A98, YELLOW_0:44; :: thesis: verum

end;

end;

end;

hence x <= d by Th28; :: thesis: verum