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