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