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 :: thesis: for x, y being object holds
( ( [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 ) )

let x, y be object ; :: 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 by ZFMISC_1:87;
A7: y in D by A5, ZFMISC_1:87;
reconsider x9 = x, y9 = y as Element of (Net-Str (D,((id the carrier of S) | D))) by A1, A5, ZFMISC_1:87;
A8: x9 = ((id the carrier of S) | D) . x9 by A3, A6, FUNCT_1:18;
y9 = ((id the carrier of S) | D) . y9 by A3, A7, FUNCT_1:18;
then (Net-Str (D,((id the carrier of S) | D))) . x9 <= (Net-Str (D,((id the carrier of S) | D))) . y9 by A2, A4, A5, A8, ORDERS_2:def 5;
then x9 <= y9 by WAYBEL11:def 10;
hence [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) by ORDERS_2:def 5; :: thesis: verum

end;

assume A9: [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 x9 = x, y9 = y as Element of (Net-Str (D,((id the carrier of S) | D))) by ZFMISC_1:87;
x9 <= y9 by A9, ORDERS_2:def 5;
then (Net-Str (D,((id the carrier of S) | D))) . x9 <= (Net-Str (D,((id the carrier of S) | D))) . y9 by WAYBEL11:def 10;
then A10: [((Net-Str (D,((id the carrier of S) | D))) . x9),((Net-Str (D,((id the carrier of S) | D))) . y9)] in the InternalRel of S by ORDERS_2:def 5;
A11: x9 = ((id the carrier of S) | D) . x9 by A1, A3;
y9 = ((id the carrier of S) | D) . y9 by A1, A3;
hence [x,y] in the InternalRel of S |_2 D by A1, A2, A9, A10, A11, 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