assume
Fr M is empty
; :: thesis: contradiction

then {} = the carrier of M \ (Int M) by SUBSET_1:def 4;

then the carrier of M c= Int M by XBOOLE_1:37;

hence contradiction by XBOOLE_0:def 10, Def6; :: thesis: verum

then {} = the carrier of M \ (Int M) by SUBSET_1:def 4;

then the carrier of M c= Int M by XBOOLE_1:37;

hence contradiction by XBOOLE_0:def 10, Def6; :: thesis: verum