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 FUNCT_2:40; :: thesis: verum