let L be non empty reflexive RelStr ; :: thesis: for D being non empty directed Subset of L
for n being Function of D,the carrier of L holds NetStr(# D,(the InternalRel of L |_2 D),n #) is prenet of L
let D be non empty directed Subset of L; :: thesis: for n being Function of D,the carrier of L holds NetStr(# D,(the InternalRel of L |_2 D),n #) is prenet of L
let n be Function of D,the carrier of L; :: thesis: NetStr(# D,(the InternalRel of L |_2 D),n #) is prenet of L
set N = NetStr(# D,(the InternalRel of L |_2 D),n #);
NetStr(# D,(the InternalRel of L |_2 D),n #) is directed
proof
let x,
y be
Element of
NetStr(#
D,
(the InternalRel of L |_2 D),
n #);
:: according to WAYBEL_0:def 1,
WAYBEL_0:def 6 :: thesis: ( not x in [#] NetStr(# D,(the InternalRel of L |_2 D),n #) or not y in [#] NetStr(# D,(the InternalRel of L |_2 D),n #) or ex b1 being Element of the carrier of NetStr(# D,(the InternalRel of L |_2 D),n #) st
( b1 in [#] NetStr(# D,(the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 ) )
assume
(
x in [#] NetStr(#
D,
(the InternalRel of L |_2 D),
n #) &
y in [#] NetStr(#
D,
(the InternalRel of L |_2 D),
n #) )
;
:: thesis: ex b1 being Element of the carrier of NetStr(# D,(the InternalRel of L |_2 D),n #) st
( b1 in [#] NetStr(# D,(the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 )
reconsider x1 =
x,
y1 =
y as
Element of
D ;
consider z1 being
Element of
L such that A1:
(
z1 in D &
x1 <= z1 &
y1 <= z1 )
by WAYBEL_0:def 1;
reconsider z =
z1 as
Element of
NetStr(#
D,
(the InternalRel of L |_2 D),
n #)
by A1;
take
z
;
:: thesis: ( z in [#] NetStr(# D,(the InternalRel of L |_2 D),n #) & x <= z & y <= z )
thus
z in [#] NetStr(#
D,
(the InternalRel of L |_2 D),
n #)
;
:: thesis: ( x <= z & y <= z )
NetStr(#
D,
(the InternalRel of L |_2 D),
n #) is
SubRelStr of
L
then reconsider N =
NetStr(#
D,
(the InternalRel of L |_2 D),
n #) as
SubRelStr of
L ;
N is
full
hence
(
x <= z &
y <= z )
by A1, YELLOW_0:61;
:: thesis: verum
end;
hence
NetStr(# D,(the InternalRel of L |_2 D),n #) is prenet of L
; :: thesis: verum