let S be non empty reflexive RelStr ; :: thesis: for D being non empty Subset of S holds Net-Str D = Net-Str D,((id the carrier of S) | D)
let D be non empty Subset of S; :: thesis: Net-Str D = Net-Str D,((id the carrier of S) | D)
set M = Net-Str D,((id the carrier of S) | D);
A1: D = the carrier of (Net-Str D,((id the carrier of S) | D)) by WAYBEL11:def 10;
A2: (id the carrier of S) | D = the mapping of (Net-Str D,((id the carrier of S) | D)) by WAYBEL11:def 10;
A3: (id the carrier of S) | D = id D by FUNCT_3:1;
A4: the InternalRel of S |_2 D c= the InternalRel of S by XBOOLE_1:17;

now

let x, y be set ; :: thesis: ( ( [x,y] in the InternalRel of S |_2 D implies [x,y] in the InternalRel of (Net-Str D,((id the carrier of S) | D)) ) & ( [x,y] in the InternalRel of (Net-Str D,((id the carrier of S) | D)) implies [x,y] in the InternalRel of S |_2 D ) )

hereby :: thesis: ( [x,y] in the InternalRel of (Net-Str D,((id the carrier of S) | D)) implies [x,y] in the InternalRel of S |_2 D )

assume A5: [x,y] in the InternalRel of S |_2 D ; :: thesis: [x,y] in the InternalRel of (Net-Str D,((id the carrier of S) | D))
then A6: ( x in D & y in D ) by ZFMISC_1:106;
reconsider x' = x, y' = y as Element of (Net-Str D,((id the carrier of S) | D)) by A1, A5, ZFMISC_1:106;
( x' = ((id the carrier of S) | D) . x' & y' = ((id the carrier of S) | D) . y' ) by A3, A6, FUNCT_1:35;
then (Net-Str D,((id the carrier of S) | D)) . x' <= (Net-Str D,((id the carrier of S) | D)) . y' by A2, A4, A5, ORDERS_2:def 9;
then x' <= y' by WAYBEL11:def 10;
hence [x,y] in the InternalRel of (Net-Str D,((id the carrier of S) | D)) by ORDERS_2:def 9; :: thesis: verum

end;

assume A7: [x,y] in the InternalRel of (Net-Str D,((id the carrier of S) | D)) ; :: thesis: [x,y] in the InternalRel of S |_2 D
then reconsider x' = x, y' = y as Element of (Net-Str D,((id the carrier of S) | D)) by ZFMISC_1:106;
x' <= y' by A7, ORDERS_2:def 9;
then (Net-Str D,((id the carrier of S) | D)) . x' <= (Net-Str D,((id the carrier of S) | D)) . y' by WAYBEL11:def 10;
then A8: [((Net-Str D,((id the carrier of S) | D)) . x'),((Net-Str D,((id the carrier of S) | D)) . y')] in the InternalRel of S by ORDERS_2:def 9;
( x' = ((id the carrier of S) | D) . x' & y' = ((id the carrier of S) | D) . y' ) by A1, A3, FUNCT_1:35;
hence [x,y] in the InternalRel of S |_2 D by A1, A2, A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;

hence Net-Str D = Net-Str D,((id the carrier of S) | D) by A1, A2, RELAT_1:def 2; :: thesis: verum