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 ) = sup (x "/\" (FinSups f)) )

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 ) = sup (x "/\" (FinSups f))

let x be Element of L; :: thesis: for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))

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

let f be Function of J, the carrier of L; :: thesis: x "/\" (Sup ) = sup (x "/\" (FinSups f))

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 ((FinSups f),L)),L ) by YELLOW_0:17;

hence x "/\" (Sup ) = x "/\" (sup (FinSups f)) by A2, Th26

.= sup ({x} "/\" (rng (netmap ((FinSups f),L)))) by A1

.= "\/" ((rng the mapping of (x "/\" (FinSups f))),L) by Th23

.= sup (x "/\" (FinSups f)) by YELLOW_2:def 5 ;

:: thesis: verum

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 ) = sup (x "/\" (FinSups f)) )

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 ) = sup (x "/\" (FinSups f))

let x be Element of L; :: thesis: for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))

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

let f be Function of J, the carrier of L; :: thesis: x "/\" (Sup ) = sup (x "/\" (FinSups f))

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 ((FinSups f),L)),L ) by YELLOW_0:17;

hence x "/\" (Sup ) = x "/\" (sup (FinSups f)) by A2, Th26

.= sup ({x} "/\" (rng (netmap ((FinSups f),L)))) by A1

.= "\/" ((rng the mapping of (x "/\" (FinSups f))),L) by Th23

.= sup (x "/\" (FinSups f)) by YELLOW_2:def 5 ;

:: thesis: verum