let I be non empty set ; for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) holds
( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi (X,i),J . i )
let J be non-Empty Poset-yielding ManySortedSet of I; for X being Subset of (product J) holds
( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi (X,i),J . i )
let X be Subset of (product J); ( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi (X,i),J . i )
hereby ( ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) implies ex_inf_of X, product J )
set f =
inf X;
assume A1:
ex_inf_of X,
product J
;
for i being Element of I holds ex_inf_of pi (X,i),J . ilet i be
Element of
I;
ex_inf_of pi (X,i),J . iA2:
inf X is_<=_than X
by A1, YELLOW_0:31;
(inf X) . i is_<=_than pi (
X,
i)
by A2, Th29;
hence
ex_inf_of pi (
X,
i),
J . i
by A3, YELLOW_0:31;
verum
end;
assume
for i being Element of I holds ex_inf_of pi (X,i),J . i
; ex_inf_of X, product J
then
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )
by Lm2;
hence
ex_inf_of X, product J
by YELLOW_0:31; verum