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