Fr [:N,M:] = [:([#] N),(Fr M):] \/ [:(Fr N),([#] M):] by Th9;
hence not [:N,M:] is without_boundary ; :: thesis: verum