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 )
A1: dom (id D) = D ;
rng (id D) = D ;
then reconsider g = id D as Function of D, the carrier of S by A1, FUNCT_2:def 1, RELSET_1:4;
(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