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 not 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 reconsider S = S as non empty 1-sorted ;
set c = the mapping of N " X;
reconsider m = the mapping of N | ( the mapping of N " X) as Function of ( the mapping of N " X),S by FUNCT_2:32;
set S = NetStr(# ( the mapping of N " X),i,m #);
A1: 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 Def6;
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 A1, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum
end;
suppose A2: 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 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 ; :: 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 A4, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum
end;
end;