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 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 ; :: thesis: 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; :: 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
A5: x in dom (netmap (FinSups f),L) and
A6: a = (netmap (FinSups f),L) . x by FUNCT_1:def 5;
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:144, YELLOW_0:34;
hence a <= "\/" (rng f),L by A6, A7; :: thesis: 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:25
.= sup (FinSups f) by YELLOW_2:def 5 ; :: thesis: verum