let L be complete LATTICE; :: thesis: for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let J be non empty set ; :: thesis: for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let K be non-empty ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let F be DoubleIndexedSet of K,L; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies rng (Infs ) is directed )
set X = rng (Infs );
assume A1: for j being Element of J holds rng (F . j) is directed ; :: thesis: rng (Infs ) is directed
for x, y being Element of L st x in rng (Infs ) & y in rng (Infs ) holds
ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )

proof

let x, y be Element of L; :: thesis: ( x in rng (Infs ) & y in rng (Infs ) implies ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z ) )
assume that
A2: x in rng (Infs ) and
A3: y in rng (Infs ) ; :: thesis: ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )
consider h being object such that
A4: h in dom (Frege F) and
A5: y = //\ (((Frege F) . h),L) by A3, Th13;
reconsider h = h as Function by A4;
reconsider H = (Frege F) . h as Function of J, the carrier of L by A4, Th10;
consider g being object such that
A6: g in dom (Frege F) and
A7: x = //\ (((Frege F) . g),L) by A2, Th13;
reconsider g = g as Function by A6;
reconsider G = (Frege F) . g as Function of J, the carrier of L by A6, Th10;
A8: ex_inf_of rng ((Frege F) . g),L by YELLOW_0:17;
defpred S₁[ object , object ] means ( $1 in J & $2 in K . $1 & ( for c being Element of L st c = (F . $1) . $2 holds
( ( for a being Element of L st a = G . $1 holds
a <= c ) & ( for b being Element of L st b = H . $1 holds
b <= c ) ) ) );
A9: for j being Element of J ex k being Element of K . j st
( G . j <= (F . j) . k & H . j <= (F . j) . k )

proof

let j be Element of J; :: thesis: ex k being Element of K . j st
( G . j <= (F . j) . k & H . j <= (F . j) . k )
j in J ;
then A10: j in dom F by PARTFUN1:def 2;
then A11: g . j in dom (F . j) by A6, Th9;
j in J ;
then A12: j in dom F by PARTFUN1:def 2;
then G . j = (F . j) . (g . j) by A6, Th9;
then A13: G . j in rng (F . j) by A11, FUNCT_1:def 3;
A14: h . j in dom (F . j) by A4, A10, Th9;
H . j = (F . j) . (h . j) by A4, A12, Th9;
then A15: H . j in rng (F . j) by A14, FUNCT_1:def 3;
rng (F . j) is directed Subset of L by A1;
then consider c being Element of L such that
A16: c in rng (F . j) and
A17: ( G . j <= c & H . j <= c ) by A13, A15, WAYBEL_0:def 1;
consider k being object such that
A18: k in dom (F . j) and
A19: c = (F . j) . k by A16, FUNCT_1:def 3;
reconsider k = k as Element of K . j by A18;
take k ; :: thesis: ( G . j <= (F . j) . k & H . j <= (F . j) . k )
thus ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A17, A19; :: thesis: verum

end;

A20: for j being object st j in J holds
ex k being object st
( k in union (rng K) & S₁[j,k] )

proof

let j9 be object ; :: thesis: ( j9 in J implies ex k being object st
( k in union (rng K) & S₁[j9,k] ) )
assume j9 in J ; :: thesis: ex k being object st
( k in union (rng K) & S₁[j9,k] )
then reconsider j = j9 as Element of J ;
consider k being Element of K . j such that
A21: ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A9;
take k ; :: thesis: ( k in union (rng K) & S₁[j9,k] )
j in J ;
then j in dom K by PARTFUN1:def 2;
then K . j in rng K by FUNCT_1:def 3;
hence k in union (rng K) by TARSKI:def 4; :: thesis: S₁[j9,k]
thus S₁[j9,k] by A21; :: thesis: verum

end;

consider f being Function such that
A22: dom f = J and
rng f c= union (rng K) and
A23: for j being object st j in J holds
S₁[j,f . j] from FUNCT_1:sch 6(A20);

A24: now :: thesis: for x being object st x in dom (doms F) holds
f . x in (doms F) . x

let x be object ; :: thesis: ( x in dom (doms F) implies f . x in (doms F) . x )
assume x in dom (doms F) ; :: thesis: f . x in (doms F) . x
then A25: x in dom F by FUNCT_6:59;
then reconsider j = x as Element of J ;
(doms F) . x = dom (F . j) by A25, FUNCT_6:22
.= K . j by FUNCT_2:def 1 ;
hence f . x in (doms F) . x by A23; :: thesis: verum

end;

dom f = dom F by A22, PARTFUN1:def 2
.= dom (doms F) by FUNCT_6:59 ;
then f in product (doms F) by A24, CARD_3:9;
then A26: f in dom (Frege F) by PARTFUN1:def 2;
then reconsider Ff = (Frege F) . f as Function of J, the carrier of L by Th10;
take z = Inf ; :: thesis: ( z in rng (Infs ) & x <= z & y <= z )
thus z in rng (Infs ) by A26, Th13; :: thesis: ( x <= z & y <= z )
A27: x = "/\" ((rng ((Frege F) . g)),L) by A7, YELLOW_2:def 6;

now :: thesis: for j being Element of J holds x <= Ff . j

let j be Element of J; :: thesis: x <= Ff . j
A28: j in J ;
then j in dom G by FUNCT_2:def 1;
then A29: G . j in rng G by FUNCT_1:def 3;
j in dom F by A28, PARTFUN1:def 2;
then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;
then A30: G . j <= Ff . j by A23;
x is_<=_than rng G by A27, A8, YELLOW_0:def 10;
then x <= G . j by A29;
hence x <= Ff . j by A30, ORDERS_2:3; :: thesis: verum

end;

hence x <= z by YELLOW_2:55; :: thesis: y <= z
A31: ex_inf_of rng ((Frege F) . h),L by YELLOW_0:17;
A32: y = "/\" ((rng ((Frege F) . h)),L) by A5, YELLOW_2:def 6;

now :: thesis: for j being Element of J holds y <= Ff . j

let j be Element of J; :: thesis: y <= Ff . j
A33: j in J ;
then j in dom H by FUNCT_2:def 1;
then A34: H . j in rng H by FUNCT_1:def 3;
j in dom F by A33, PARTFUN1:def 2;
then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;
then A35: H . j <= Ff . j by A23;
y is_<=_than rng H by A32, A31, YELLOW_0:def 10;
then y <= H . j by A34;
hence y <= Ff . j by A35, ORDERS_2:3; :: thesis: verum

end;

hence y <= z by YELLOW_2:55; :: thesis: verum

end;

hence rng (Infs ) is directed by WAYBEL_0:def 1; :: thesis: verum