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 ((),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup ()

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 ((),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup ()

let f be Function of J, the carrier of L; :: thesis: ( ex_sup_of rng f,L & ex_sup_of rng (netmap ((),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) implies Sup = sup () )
assume that
A1: ex_sup_of rng f,L and
A2: ex_sup_of rng (netmap ((),L)),L and
A3: for x being Element of Fin J holds ex_sup_of f .: x,L ; :: thesis: Sup = sup ()
set h = netmap ((),L);
A4: "\/" ((rng f),L) <= sup (rng (netmap ((),L))) by ;
rng (netmap ((),L)) is_<=_than "\/" ((rng f),L)
proof
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng (netmap ((),L)) or a <= "\/" ((rng f),L) )
assume a in rng (netmap ((),L)) ; :: thesis: a <= "\/" ((rng f),L)
then consider x being object such that
A5: x in dom (netmap ((),L)) and
A6: a = (netmap ((),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 ;
hence a <= "\/" ((rng f),L) by A6, A7; :: thesis: verum
end;
then A8: sup (rng (netmap ((),L))) <= "\/" ((rng f),L) by ;
thus Sup = "\/" ((rng f),L) by YELLOW_2:def 5
.= sup (rng (netmap ((),L))) by
.= sup () by YELLOW_2:def 5 ; :: thesis: verum