let N, M be non empty locally_euclidean TopSpace; 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
; verum