Int [:N,M:] = [:(Int N),(Int M):] by Th8
.= [: the carrier of N,(Int M):] by Def6
.= [: the carrier of N, the carrier of M:] by Def6
.= the carrier of [:N,M:] by BORSUK_1:def 2 ;
hence [:N,M:] is without_boundary ; :: thesis: verum