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