let E be set ; :: thesis: ( E is MC-closed implies not E is empty )
assume E is MC-closed ; :: thesis: not E is empty
then E is with_FALSUM by Def7;
hence not E is empty by Def1; :: thesis: verum