M c= M ;
hence ( ( B <> {} implies meet B is Subset of ) & ( not B <> {} implies M is Subset of ) ) ; :: thesis: verum