let L be non empty reflexive antisymmetric complete RelStr ; :: thesis: ( ( for x being Element of
for N being prenet of st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) ) implies for x being Element of
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
for N being prenet of st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) ; :: thesis: for x being Element of
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 ; :: 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
consider g being Function of Fin J,the carrier of L;