let it1, it2 be strict SubNetStr of N; :: thesis: ( it1 is full SubRelStr of N & the carrier of it1 = the mapping of N " X & it2 is full SubRelStr of N & the carrier of it2 = the mapping of N " X implies it1 = it2 )
assume that
A5: it1 is full SubRelStr of N and
A6: the carrier of it1 = the mapping of N " X and
A7: it2 is full SubRelStr of N and
A8: the carrier of it2 = the mapping of N " X ; :: thesis: it1 = it2
A9: the mapping of it1 = the mapping of N | the carrier of it2 by A6, A8, Def6
.= the mapping of it2 by Def6 ;
RelStr(# the carrier of it1, the InternalRel of it1 #) = RelStr(# the carrier of it2, the InternalRel of it2 #) by A5, A6, A7, A8, YELLOW_0:57;
hence it1 = it2 by A9; :: thesis: verum