let L be non empty reflexive antisymmetric RelStr ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 & ex_sup_of rng (netmap (FinSups f),L),L ) and
A2: for x being Element of Fin J holds ex_sup_of f .: x,L ; :: thesis: Sup = sup (FinSups f)
set h = netmap (FinSups f),L;
A3: "\/" (rng f),L <= sup (rng (netmap (FinSups f),L)) by A1, Th25, YELLOW_0:34;
rng (netmap (FinSups f),L) is_<=_than "\/" (rng f),L

proof

let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng (netmap (FinSups f),L) or a <= "\/" (rng f),L )
assume a in rng (netmap (FinSups f),L) ; :: thesis: a <= "\/" (rng f),L
then consider x being set such that
A4: ( x in dom (netmap (FinSups f),L) & a = (netmap (FinSups f),L) . x ) by FUNCT_1:def 5;
consider g being Function of (Fin J),the carrier of L such that
A5: for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
reconsider x = x as Element of Fin J by A4, A5;
ex_sup_of f .: x,L by A2;
then sup (f .: x) <= "\/" (rng f),L by A1, RELAT_1:144, YELLOW_0:34;
hence a <= "\/" (rng f),L by A4, A5; :: thesis: verum

end;

then A6: sup (rng (netmap (FinSups f),L)) <= "\/" (rng f),L by A1, YELLOW_0:def 9;
thus Sup = "\/" (rng f),L by YELLOW_2:def 5
.= sup (rng (netmap (FinSups f),L)) by A3, A6, ORDERS_2:25
.= sup (FinSups f) by YELLOW_2:def 5 ; :: thesis: verum