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