let S be non empty reflexive RelStr ; 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; 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 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 ;
( ( [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 ( [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
;
[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;
verum
end; assume A9:
[x,y] in the
InternalRel of
(Net-Str (D,((id the carrier of S) | D)))
;
[x,y] in the InternalRel of S |_2 Dthen 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;
verum end;
hence
Net-Str D = Net-Str (D,((id the carrier of S) | D))
by A1, A2, RELAT_1:def 2; verum