let S be non empty reflexive RelStr ; :: thesis: for D being non empty directed Subset of S
for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j )
let D be non empty directed Subset of S; :: thesis: for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j )
( dom (id D) = D & rng (id D) = D ) by RELAT_1:71;
then reconsider g = id D as Function of D,the carrier of S by FUNCT_2:def 1, RELSET_1:11;
(id the carrier of S) | D = id D by FUNCT_3:1;
then Net-Str D = Net-Str D,g by WAYBEL17:9;
hence for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j ) by WAYBEL11:def 10; :: thesis: verum