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 #);
:: 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
(
x in [#] NetStr(#
(Fin J),
(RelIncl (Fin J)),
g #) &
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)) ;
(
x c= z &
y c= z )
by XBOOLE_1:7;
then
(
x2 <= z1 &
y2 <= z1 )
by YELLOW_1:3;
hence
(
x <= z &
y <= z )
by A3, YELLOW_0:1;
:: 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