set c = the mapping of N " X;
reconsider i = the InternalRel of N |_2 ( the mapping of N " X) as Relation of ( the mapping of N " X),( the mapping of N " X) ;
per cases
( not S is empty or S is empty )
;
suppose A2:
S is
empty
;
ex b1 being strict SubNetStr of N st
( b1 is full SubRelStr of N & the carrier of b1 = the mapping of N " X )then
the
mapping of
N = {}
;
then
the
mapping of
N " X = {}
;
then reconsider m =
{} as
Function of
( the mapping of N " X),
S by RELSET_1:12;
set S =
NetStr(#
( the mapping of N " X),
i,
m #);
A3:
the
mapping of
NetStr(#
( the mapping of N " X),
i,
m #)
= the
mapping of
N | the
carrier of
NetStr(#
( the mapping of N " X),
i,
m #)
by A2;
A4:
i c= the
InternalRel of
N
by XBOOLE_1:17;
then
NetStr(#
( the mapping of N " X),
i,
m #) is
SubRelStr of
N
by YELLOW_0:def 13;
then reconsider S =
NetStr(#
( the mapping of N " X),
i,
m #) as
strict SubNetStr of
N by A3, Def6;
take
S
;
( S is full SubRelStr of N & the carrier of S = the mapping of N " X )thus
(
S is
full SubRelStr of
N & the
carrier of
S = the
mapping of
N " X )
by A4, YELLOW_0:def 13, YELLOW_0:def 14;
verum end; end;