let L be non empty reflexive transitive 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 net 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 net of L
let n be Function of D, the carrier of L; :: thesis: NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L
set N = NetStr(# D,( the InternalRel of L |_2 D),n #);
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;
reconsider N = N as full SubRelStr of L by YELLOW_0:def 14;
N is directed
proof
let x, y be Element of N; :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] N or not y in [#] N or ex b1 being Element of the carrier of N st
( b1 in [#] N & x <= b1 & y <= b1 ) )
assume that
x in [#] N and
y in [#] N ; :: thesis: ex b1 being Element of the carrier of N st
( b1 in [#] 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 N by A1;
take z ; :: thesis: ( z in [#] N & x <= z & y <= z )
thus z in [#] N ; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A2, YELLOW_0:60; :: thesis: verum
end;
then reconsider N = N as prenet of L ;
N is transitive ;
hence NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L ; :: thesis: verum