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 FUNCT_2:sch 8(A1);
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 #);
WAYBEL_0:def 1,
WAYBEL_0:def 6 ( 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 #)
;
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
;
( z in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= z & y <= z )
thus
z in [#] NetStr(#
(Fin J),
(RelIncl (Fin J)),
g #)
;
( 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;
verum
end;
then reconsider M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) as prenet of L ;
take
M
; 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; verum