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
S is
empty
;
:: thesis: 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
carrier of
S = {}
;
then
the
mapping of
N = {}
;
then A2:
the
mapping of
N " X = {}
by RELAT_1:172;
then reconsider m =
{} as
Function of
(the mapping of N " X),the
carrier of
S by RELSET_1:25;
set S =
NetStr(#
(the mapping of N " X),
i,
m #);
A3:
i c= the
InternalRel of
N
by XBOOLE_1:17;
then A4:
NetStr(#
(the mapping of N " X),
i,
m #) is
SubRelStr of
N
by YELLOW_0:def 13;
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;
then reconsider S =
NetStr(#
(the mapping of N " X),
i,
m #) as
strict SubNetStr of
N by A4, Def8;
take
S
;
:: thesis: ( 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 A3, YELLOW_0:def 13, YELLOW_0:def 14;
:: thesis: verum end;