Fr M = the carrier of M \ (Int M) by SUBSET_1:def 4
.= the carrier of M \ the carrier of M by Def6
.= {} by XBOOLE_1:37 ;
hence Fr M is empty ; :: thesis: verum