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;

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 ) )

hence
Net-Str D = Net-Str (D,((id the carrier of S) | D))
by A1, A2, RELAT_1:def 2; :: thesis: verum( ( [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 ) )

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;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 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 Dassume 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;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

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