let N, M be non empty locally_euclidean TopSpace; :: thesis: Fr [:N,M:] = [:([#] N),(Fr M):] \/ [:(Fr N),([#] M):]
thus Fr [:N,M:] = ([#] [:N,M:]) \ (Int [:N,M:]) by SUBSET_1:def 4
.= [:([#] N),([#] M):] \ (Int [:N,M:]) by BORSUK_1:def 2
.= [:([#] N),([#] M):] \ [:(Int N),(Int M):] by Th8
.= [:(([#] N) \ (Int N)),([#] M):] \/ [:([#] N),(([#] M) \ (Int M)):] by ZFMISC_1:103
.= [:(([#] N) \ (Int N)),([#] M):] \/ [:([#] N),(Fr M):] by SUBSET_1:def 4
.= [:([#] N),(Fr M):] \/ [:(Fr N),([#] M):] by SUBSET_1:def 4 ; :: thesis: verum