let L be non empty reflexive antisymmetric RelStr ; for J being set
for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup (FinSups f)
let J be set ; for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup (FinSups f)
let f be Function of J, the carrier of L; ( ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) implies Sup = sup (FinSups f) )
assume that
A1:
ex_sup_of rng f,L
and
A2:
ex_sup_of rng (netmap ((FinSups f),L)),L
and
A3:
for x being Element of Fin J holds ex_sup_of f .: x,L
; Sup = sup (FinSups f)
set h = netmap ((FinSups f),L);
A4:
"\/" ((rng f),L) <= sup (rng (netmap ((FinSups f),L)))
by A1, A2, Th25, YELLOW_0:34;
rng (netmap ((FinSups f),L)) is_<=_than "\/" ((rng f),L)
proof
let a be
Element of
L;
LATTICE3:def 9 ( not a in rng (netmap ((FinSups f),L)) or a <= "\/" ((rng f),L) )
assume
a in rng (netmap ((FinSups f),L))
;
a <= "\/" ((rng f),L)
then consider x being
object such that A5:
x in dom (netmap ((FinSups f),L))
and A6:
a = (netmap ((FinSups f),L)) . x
by FUNCT_1:def 3;
A7:
ex
g being
Function of
(Fin J), the
carrier of
L st
for
x being
Element of
Fin J holds
(
g . x = sup (f .: x) &
FinSups f = NetStr(#
(Fin J),
(RelIncl (Fin J)),
g #) )
by Def2;
then reconsider x =
x as
Element of
Fin J by A5;
ex_sup_of f .: x,
L
by A3;
then
sup (f .: x) <= "\/" (
(rng f),
L)
by A1, RELAT_1:111, YELLOW_0:34;
hence
a <= "\/" (
(rng f),
L)
by A6, A7;
verum
end;
then A8:
sup (rng (netmap ((FinSups f),L))) <= "\/" ((rng f),L)
by A2, YELLOW_0:def 9;
thus Sup =
"\/" ((rng f),L)
by YELLOW_2:def 5
.=
sup (rng (netmap ((FinSups f),L)))
by A4, A8, ORDERS_2:2
.=
sup (FinSups f)
by YELLOW_2:def 5
; verum