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 ;
hence not E is empty ; :: thesis: verum