let L be non empty reflexive RelStr ; 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; 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; 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 #);
WAYBEL_0:def 1,
WAYBEL_0:def 6 ( 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 that
x in [#] NetStr(#
D,
( the InternalRel of L |_2 D),
n #)
and
y in [#] NetStr(#
D,
( the InternalRel of L |_2 D),
n #)
;
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
and A2:
(
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
;
( 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 #)
;
( x <= z & y <= z )
the
InternalRel of
NetStr(#
D,
( the InternalRel of L |_2 D),
n #)
c= the
InternalRel of
L
by XBOOLE_1:17;
then reconsider N =
NetStr(#
D,
( the InternalRel of L |_2 D),
n #) as
SubRelStr of
L by YELLOW_0:def 13;
N is
full
;
hence
(
x <= z &
y <= z )
by A2, YELLOW_0:60;
verum
end;
hence
NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L
; verum