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

.= the carrier of M \ the carrier of M by Def6

.= {} by XBOOLE_1:37 ;

hence Fr M is empty ; :: thesis: verum