deffunc H1( Element of Fin J) -> Element of the carrier of L = sup (f .: \$1);
A1: for x being Element of Fin J holds H1(x) in the carrier of L ;
consider g being Function of (Fin J), the carrier of L such that
A2: for x being Element of Fin J holds g . x = H1(x) from set M = NetStr(# (Fin J),(RelIncl (Fin J)),g #);
NetStr(# (Fin J),(RelIncl (Fin J)),g #) is directed
proof
let x, y be Element of NetStr(# (Fin J),(RelIncl (Fin J)),g #); :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) or not y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) or ex b1 being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st
( b1 in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b1 & y <= b1 ) )

assume that
x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) and
y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; :: thesis: ex b1 being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st
( b1 in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b1 & y <= b1 )

reconsider x1 = x, y1 = y as Element of Fin J ;
reconsider z = x1 \/ y1 as Element of NetStr(# (Fin J),(RelIncl (Fin J)),g #) ;
take z ; :: thesis: ( z in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= z & y <= z )
thus z in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; :: thesis: ( x <= z & y <= z )
A3: InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) by YELLOW_1:def 1;
then reconsider x2 = x, y2 = y, z1 = z as Element of (InclPoset (Fin J)) ;
y c= z by XBOOLE_1:7;
then A4: y2 <= z1 by YELLOW_1:3;
x c= z by XBOOLE_1:7;
then x2 <= z1 by YELLOW_1:3;
hence ( x <= z & y <= z ) by ; :: thesis: verum
end;
then reconsider M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) as prenet of L ;
take M ; :: thesis: 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) & M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )

thus 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) & M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by A2; :: thesis: verum