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