let L be non empty reflexive antisymmetric complete RelStr ; :: thesis: ( ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ()) )

assume A1: for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; :: thesis: for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ())

let x be Element of L; :: thesis: for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ())

let J be set ; :: thesis: for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ())
let f be Function of J, the carrier of L; :: thesis: x "/\" () = sup (x "/\" ())
set F = FinSups f;
A2: for x being Element of Fin J holds ex_sup_of f .: x,L by YELLOW_0:17;
( ex_sup_of rng f,L & ex_sup_of rng (netmap ((),L)),L ) by YELLOW_0:17;
hence x "/\" () = x "/\" (sup ()) by
.= sup ({x} "/\" (rng (netmap ((),L)))) by A1
.= "\/" ((rng the mapping of (x "/\" ())),L) by Th23
.= sup (x "/\" ()) by YELLOW_2:def 5 ;
:: thesis: verum