take N ; :: thesis: ( N is SubRelStr of N & the mapping of N = the mapping of N | the carrier of N )
thus N is SubRelStr of N by Th15; :: thesis: the mapping of N = the mapping of N | the carrier of N
thus the mapping of N = the mapping of N | the carrier of N by RELSET_1:34; :: thesis: verum