deffunc H_{1}( Element of Fin J) -> Element of the carrier of L = sup (f .: $1);

A1: for x being Element of Fin J holds H_{1}(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 = H_{1}(x)
from FUNCT_2:sch 8(A1);

set M = NetStr(# (Fin J),(RelIncl (Fin J)),g #);

NetStr(# (Fin J),(RelIncl (Fin J)),g #) is directed

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

A1: for x being Element of Fin J holds H

consider g being Function of (Fin J), the carrier of L such that

A2: for x being Element of Fin J holds g . x = H

set M = NetStr(# (Fin J),(RelIncl (Fin J)),g #);

NetStr(# (Fin J),(RelIncl (Fin J)),g #) is directed

proof

then reconsider M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) as prenet of L ;
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 b_{1} being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st

( b_{1} in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b_{1} & y <= b_{1} ) )

assume that

x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) and

y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; :: thesis: ex b_{1} being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st

( b_{1} in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b_{1} & y <= b_{1} )

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 A3, A4, YELLOW_0:1; :: thesis: verum

end;( b

assume that

x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) and

y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; :: thesis: ex b

( b

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 A3, A4, YELLOW_0:1; :: thesis: verum

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